3 ms·

Yep. ESBMC and PolySpace both work for C++. I use CBMC for C. They run an abstract machine model through an SMT solver. Among other things, this abstract mach

Yep. ESBMC and PolySpace both work for C++. I use CBMC for C. They run an abstract machine model through an SMT solver. Among other things, this abstract machine model tracks memory usage, UAF, aliasing, etc. With custom assertions, it can also cover issues like casting safety, serialization issues, logic errors, etc. More or less, you can build up any proof obligations you need and run them through the model checker. It will provide counter-examples if it detects a failure.

erik_seaberg 2y ago
I'm definitely digging into this, thank you! I'm a little concerned about ESBMC's "simulating a finite prefix of the program execution with all possible inputs" when important software like operating systems are intended to run indefinitely. Would they start with a valid state (filesystem, process list) and prove no invalid state is reachable within n syscalls or interrupts? Maybe I was hoping for proving invariants.
- nanolith 2y ago
  So, the way I deal with this is to provide an exit condition in the loop that is triggered in a non-deterministic finite way by the model checker but that is not triggered at runtime. This allows for termination, which is required as part of the model check, while maintaining the loop. The best way that I've found to model check software is to decompose the software by function, defining function contracts and invariants along the way. To reduce complexity, shadow functions that follow the same function contracts and maintain the same invariants can be substituted. A shadow function uses non-determinism to exercise the same range of behaviors that the real function provides in a way that is simpler for the model checker to verify. When verifying a function with the model checker, you can substitute functions it calls with these shadow functions to reduce the complexity of the model check. The example server I'm using for the book initiates a TLS connection with the client. Each connection is maintained by a fiber that enters into a command-response loop. When verifying this loop function in the model checker, I can shadow the functions that read the command and send the response. As long as these shadows follow the same function contract as the function, I can verify that the loop function is correct. For instance, the read command function returns a command in the output variable on success that must be freed by the caller. The dispatch function that dispatches the command and sends the response expects this command to be valid and treats it as read-only data with a lifetime that is beyond the lifetime of the dispatch function. Finally, the loop cleans up the command. All of this can be specified using the function contracts defined by this function as well as the semantics of the real functions and the shadow functions. We know based on the contracts that we expect this command object to be created on success, and we know based on the abstract model that it must be cleaned up. If, for instance, we freed it before calling dispatch, the abstract model would find a UAF counter-example. If this sounds like a lot, there is a reason why I'm writing a book on the topic of practical model checking in C, with a mature well-worked example that mirrors a real-world application.
rich_sasha 2y ago
How very interesting. Does that detect issues at runtime, or prove statically that the code is "safe" (whatever the remit of that definition is here)? If the former, I guess you're still at the mercy of test coverage and all the pitfalls it entails.
- nanolith 2y ago
  Model checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how linting works. This is significantly more advanced. The model checker translates an abstract model of execution for the code into an SMT solver, and uses this to find counter-examples. The SMT solver works backward from failure cases to discover a combination of inputs or program state that can cause any one of these failure cases. This traces memory, data flow, and control flow. It's actually a pretty neat thing. It doesn't require existing test coverage or anything at runtime to work.

erik_seaberg 2y ago

I'm definitely digging into this, thank you! I'm a little concerned about ESBMC's "simulating a finite prefix of the program execution with all possible inputs" when important software like operating systems are intended to run indefinitely. Would they start with a valid state (filesystem, process list) and prove no invalid state is reachable within n syscalls or interrupts? Maybe I was hoping for proving invariants.

nanolith 2y ago
So, the way I deal with this is to provide an exit condition in the loop that is triggered in a non-deterministic finite way by the model checker but that is not triggered at runtime. This allows for termination, which is required as part of the model check, while maintaining the loop. The best way that I've found to model check software is to decompose the software by function, defining function contracts and invariants along the way. To reduce complexity, shadow functions that follow the same function contracts and maintain the same invariants can be substituted. A shadow function uses non-determinism to exercise the same range of behaviors that the real function provides in a way that is simpler for the model checker to verify. When verifying a function with the model checker, you can substitute functions it calls with these shadow functions to reduce the complexity of the model check. The example server I'm using for the book initiates a TLS connection with the client. Each connection is maintained by a fiber that enters into a command-response loop. When verifying this loop function in the model checker, I can shadow the functions that read the command and send the response. As long as these shadows follow the same function contract as the function, I can verify that the loop function is correct. For instance, the read command function returns a command in the output variable on success that must be freed by the caller. The dispatch function that dispatches the command and sends the response expects this command to be valid and treats it as read-only data with a lifetime that is beyond the lifetime of the dispatch function. Finally, the loop cleans up the command. All of this can be specified using the function contracts defined by this function as well as the semantics of the real functions and the shadow functions. We know based on the contracts that we expect this command object to be created on success, and we know based on the abstract model that it must be cleaned up. If, for instance, we freed it before calling dispatch, the abstract model would find a UAF counter-example. If this sounds like a lot, there is a reason why I'm writing a book on the topic of practical model checking in C, with a mature well-worked example that mirrors a real-world application.

rich_sasha 2y ago

How very interesting. Does that detect issues at runtime, or prove statically that the code is "safe" (whatever the remit of that definition is here)? If the former, I guess you're still at the mercy of test coverage and all the pitfalls it entails.

nanolith 2y ago
Model checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how linting works. This is significantly more advanced. The model checker translates an abstract model of execution for the code into an SMT solver, and uses this to find counter-examples. The SMT solver works backward from failure cases to discover a combination of inputs or program state that can cause any one of these failure cases. This traces memory, data flow, and control flow. It's actually a pretty neat thing. It doesn't require existing test coverage or anything at runtime to work.