4 ms·

Leave it to politicians to pit bull a language. Model checked C/C++ is memory safe. Had they reached out to a wider set of people for guidance, they'd have a mo

Leave it to politicians to pit bull a language. Model checked C/C++ is memory safe. Had they reached out to a wider set of people for guidance, they'd have a more balanced report. I will agree that software safety -- not just memory safety -- is critical. Trying to attack this at the language level instead of the development process and assurance level is daft. FIPS certification and aerospace certification both require auditing already. It's not much of a stretch to require an audit of critical infrastructure to verify that safety processes are in place. Simply adopting a different language won't make software safe. It will make it safer, perhaps, but we can do better. Model checked code -- be it written in Rust, C, or C++ -- is on the same level. Tools exist for each. That is what CISA should focus on, not trying to force organizations to migrate their code bases to some new and shiny language.

erik_seaberg 2y ago
I'm a little familiar with TLA+ but it can't verify the actual code you want to run, only a restatement of your intended algorithm. Are there published model checkers that can check real C++? How would they catch double-free or use-after-free or double-throw?
- nanolith 2y ago
  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.
timClicks 2y ago
That's the intent of the document - to reach people for guidance. The document under discussion is requesting comment from industry.
- nanolith 2y ago
  Yep. I'm writing up a response letter based on my own work with model checked C. It's not the language but the process and the tooling that matters. It is definitely true that the industry has been quite lax with memory safety, but the solution isn't to rewrite everything in yet another language. The solution is to tighten development processes and put forward a plan to make existing code safer.
  - dataflow 2y ago
    > It's not the language but the process and the tooling that matters. You're missing some other critical components: the developers, and the costs. If you come up with processes and tooling that is difficult to use widely, you're going to negatively impact your ability to deliver. That's not a trade-off you can ignore. If the cost of using C++ safely ends up being that only (say) 10% of the developers who currently use it will be able to keep doing that -- that on its own might justify a government policy decision to avoid it completely. > but the solution isn't to rewrite everything in yet another language How many times more effort would it be to rewrite a typical C++ function in a memory-safe language vs. verify the equivalent guarantees with model-checking tools, in your view? Like how much actual work are you saving here? And how do the resulting turnaround times (say, compile/verification/etc. times) compare?
    - nanolith 2y ago
      > You're missing some other critical components: the developers, and the costs. No, I'm not. > If you come up with processes and tooling that is difficult to use widely, That's an unfounded assumption. The tooling and processes I have developed are no more difficult to use than unit testing. > How many times more effort would it be... I'd say compared to the 10% or so overhead of model checking, it would be approximately 8X as difficult, given that this requires learning a new language, using it correctly, and rebuilding the semantics in a way that is safe in that language. But, first, you need to learn new frameworks, rebuild all of the testing and quality assurance that went into the first development process, and rebuild the same level of trust as the original. Writing software is the easy part. It's all of the other stuff, like analysis, testing, confidence building, and engineering that costs money, and this would have to be redone from scratch, as the artifact from that original effort is being thrown away for a rewrite. Remember: the cost of rewriting software isn't just the cost of sitting down and banging out code. > And how do the resulting turnaround times (say, compile/verification/etc. times) compare? Model checking is actually pretty fast if you use proper shadowing. Compiling with C is lightning fast. I'd say that using a model checker is a little slower than compiling with Rust. Also, you are mistaken that using a memory-safe language gives equivalent guarantees. It does not. A model checker allows you to write safer code. There are more errors than memory errors. Memory safety fixes many of the problems, but not nearly enough. So, after that rewrite, you'll also need to add a model checker or some other kind of formal methods to be as safe as just using the model checker to begin with. For Rust, that's Kani. It's not an apples to apples comparison.

erik_seaberg 2y ago

I'm a little familiar with TLA+ but it can't verify the actual code you want to run, only a restatement of your intended algorithm. Are there published model checkers that can check real C++? How would they catch double-free or use-after-free or double-throw?

nanolith 2y ago
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.

timClicks 2y ago

That's the intent of the document - to reach people for guidance. The document under discussion is requesting comment from industry.

nanolith 2y ago
Yep. I'm writing up a response letter based on my own work with model checked C. It's not the language but the process and the tooling that matters. It is definitely true that the industry has been quite lax with memory safety, but the solution isn't to rewrite everything in yet another language. The solution is to tighten development processes and put forward a plan to make existing code safer.
- dataflow 2y ago
  > It's not the language but the process and the tooling that matters. You're missing some other critical components: the developers, and the costs. If you come up with processes and tooling that is difficult to use widely, you're going to negatively impact your ability to deliver. That's not a trade-off you can ignore. If the cost of using C++ safely ends up being that only (say) 10% of the developers who currently use it will be able to keep doing that -- that on its own might justify a government policy decision to avoid it completely. > but the solution isn't to rewrite everything in yet another language How many times more effort would it be to rewrite a typical C++ function in a memory-safe language vs. verify the equivalent guarantees with model-checking tools, in your view? Like how much actual work are you saving here? And how do the resulting turnaround times (say, compile/verification/etc. times) compare?
  - nanolith 2y ago
    > You're missing some other critical components: the developers, and the costs. No, I'm not. > If you come up with processes and tooling that is difficult to use widely, That's an unfounded assumption. The tooling and processes I have developed are no more difficult to use than unit testing. > How many times more effort would it be... I'd say compared to the 10% or so overhead of model checking, it would be approximately 8X as difficult, given that this requires learning a new language, using it correctly, and rebuilding the semantics in a way that is safe in that language. But, first, you need to learn new frameworks, rebuild all of the testing and quality assurance that went into the first development process, and rebuild the same level of trust as the original. Writing software is the easy part. It's all of the other stuff, like analysis, testing, confidence building, and engineering that costs money, and this would have to be redone from scratch, as the artifact from that original effort is being thrown away for a rewrite. Remember: the cost of rewriting software isn't just the cost of sitting down and banging out code. > And how do the resulting turnaround times (say, compile/verification/etc. times) compare? Model checking is actually pretty fast if you use proper shadowing. Compiling with C is lightning fast. I'd say that using a model checker is a little slower than compiling with Rust. Also, you are mistaken that using a memory-safe language gives equivalent guarantees. It does not. A model checker allows you to write safer code. There are more errors than memory errors. Memory safety fixes many of the problems, but not nearly enough. So, after that rewrite, you'll also need to add a model checker or some other kind of formal methods to be as safe as just using the model checker to begin with. For Rust, that's Kani. It's not an apples to apples comparison.