[HN Gopher] CBMC: C bounded model checker (2021)
___________________________________________________________________
CBMC: C bounded model checker (2021)
Author : fanf2
Score : 74 points
Date : 2024-05-04 13:42 UTC (9 hours ago)
(HTM) web link (www.cprover.org)
(TXT) w3m dump (www.cprover.org)
| quotemstr wrote:
| Wouldn't this project be more usefully done at the LLVM IR level
| so we could plug in any existing LLVM frontend and gain full
| support for language features like C++ templates?
| flohofwoe wrote:
| My guess is that LLVM IR preserves too little semantic
| information to implement such a feature.
| SnowflakeOnIce wrote:
| It predates LLVM. That's one reason, anyway.
| rjmunro wrote:
| I think the LLVM level doesn't work as it throws away too much
| semantic information, but much of the CLANG front end can be
| used via it's API.
|
| There is a fork of CBMC called ESBMC that does this and many
| other changes:
| https://ssvlab.github.io/esbmc/documentation.html
| quotemstr wrote:
| I'm curious about what relevant details get thrown away in
| translation to LLVM IR and that we can't add back with
| annotations. It's a shame that it's not possible to use these
| analysis tools on modern C++ codebases.
| rocqua wrote:
| Undefined behavior around void pointers springs to mind.
| nickpsecurity wrote:
| Another problem with LLVM I've heard about is that it's
| intermediate language or API or something is a moving,
| informally-specified target. People who know LLVM internals
| might weigh in on that claim. If true, it's actually easier to
| target C or a subset of Rust just because it's static and well-
| understood.
|
| Two projects sought to mitigate these issues by going in
| different directions. One was a compiler backend that aimed to
| be easy to learn with well-specified IL. The other aimed to
| formalize LLVM's IL.
|
| http://c9x.me/compile/
|
| https://github.com/AliveToolkit/alive2
|
| There have also been typed, assembly languages to support
| verification from groups like FLINT. One can also compile
| language-specific analysis with a certified to LLVM IL
| compiler. Integrating pieces from different languages can have
| risks. That (IIRC) is being mitigated by people doing secure,
| abstract compilation.
| tkz1312 wrote:
| klee is a similar tool that operates on llvm bytecode:
| http://klee-se.org/
| IshKebab wrote:
| I've used this before. It's pretty great. Also used as the
| backend for Kani I believe (Amazon's Rust formal verification
| tool).
| PartiallyTyped wrote:
| This is achieved by latching on to rustc, and then compiling to
| gotoc, which is then used with CBMC.
|
| Removed due to my misunderstanding:
|
| ~~I don't think Kani counts as a "formal" verification tool,
| emphasis on "formal", but it is a verification tool for rust
| code and is powered by CBMC.~~
| IshKebab wrote:
| I'm not sure what you're implying. Kani absolutely is formal
| verification. CBMC stands for C Bounded Model Checker and
| model checking is one of the main forms of formal
| verification.
| PartiallyTyped wrote:
| Edit:
|
| Seems like I misread the documentation...
|
| ~~What I was implying is that Kani just can't figure out
| all of the paths;~~ ~~Consider this example from Kani
| documentation [1]:~~ fn estimate_size(x:
| u32) -> u32 { if x < 256 { if x
| < 128 { return 1; }
| else { return 3; }
| } else if x < 1024 { if x > 1022 {
| panic!("Oh no, a failing corner case!"); }
| else { return 5; }
| } else { if x < 2048 {
| return 7; } else {
| return 9; } } }
|
| ~~Kani is very unlikely to find x=1023.~~
|
| https://model-checking.github.io/kani/tutorial-first-
| steps.h...
| accelbred wrote:
| Kani will find 1023 unless you constrain the input. The
| link you posted is saying a property test is unlikely to
| find it but Kani will find it.
| IshKebab wrote:
| Yeah you misread that. Read it again, it's saying normal
| fuzzing is unlikely to find it but Kani finds it
| instantly.
| PartiallyTyped wrote:
| Oh this is embarrassing.
| mrnoone wrote:
| Some other tool (Coq-based) to formally verify unsafe Rust
| https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev
| PartiallyTyped wrote:
| CBMC also powers Kani <3
| ranger_danger wrote:
| How does this compare to scan-build, clazy etc.?
| IshKebab wrote:
| Those are different kinds of tools. Clazy is pretty much a
| linter. Scan-build is a traditional static analyser. It tries
| to find bugs or possible bugs but it's not trying to disprove
| the presence of bugs.
|
| CBMC is a formal verification tool which tries to _prove_ that
| there aren 't any bugs (where "bugs" means things like UB).
| xxmarkuski wrote:
| CBMC ist pretty cool, I've used it in my bachelor's thesis for
| verification of fairness properties in proportional voting.
| Another use case I've seen is using CBMC in multiparty
| computation. What you have there is methods that work on boolean
| circuits. Flange CBMC in front of this and you got multiparty
| computation of C code.
| nanolith wrote:
| I have been using CBMC to formally verify C for six, make that
| seven years now (edit: time flies). The latest release is
| actually pretty good.
|
| The secret to model checking is to understand that you're
| building and verifying a specification in code. It works best if
| specifications are built function by function. For each function,
| I'll build "shadow functions" that simplify any functions it
| calls with a range of potential non-deterministic behavior that
| matches that function's contract. In this way, formal
| specifications can be built from the ground up by first verifying
| a lower-level function and then replacing it with a shadow
| function that mimics its behavior in a non-deterministic but SMT
| solver friendly way.
|
| There are things that model checking doesn't do well. Anything
| with recursion or looping that can't be easily broken down will
| not perform well with a model checker. While algorithms like
| balanced binary trees or sorting can be broken down in a way that
| can be model checked, other algorithms may require the sort of
| induction one gets with constructive proofs to sufficiently
| verify. There is an art to this which will lead to style changes
| in C and a slightly different way of building up functions from
| pieces that can be trivially model checked. Honestly, that's not
| a bad thing.
|
| For the parts that can't be easily model checked, I'm working on
| a C parser library that can be formally verified, which will
| import C directly into Coq or Lean. I consider that the "last
| mile" before formal methods in firmware and system software is to
| the point that it's generally available.
___________________________________________________________________
(page generated 2024-05-04 23:00 UTC)