Introduction about Calysto

Calysto is a scalable and precise static checker for general purpose code, as it is written today — meaning that it does not require users to write interface specifications and pre/post-conditions. Calysto checks pointer properties and user provided assertions.

Calysto works on the SSA form, and as such is language independent. However, interpretation of library functions (like C-lib and STL) as well as trace reporting is language-dependent (for instance, demangling C++ and Java names). Currently, trace reports are readable only for languages that do not mangle names (like C).

Since specifications rarely exist, and software is usually a flux of synchronizations between the actual code and mental models of all the programmers working on the project, it is a bit inappropriate to claim that general applications, like Linux kernel, can be formally verified. So, I consider Calysto a bug hunting companion, rather than a formal verification tool.

Story

Callisto was a hunting companion of Artemis — goddess of hunt in Greek mythology. Calysto is an intentionally misspelled version (so that it’s easier to find).

Key Ideas

There are several key ideas in Calysto:

I have noticed that most false positives in the Saturn version that I used for comparison came from the lack of interprocedural path-sensitivity. Calysto features a novel abstraction, which I dubbed structural abstraction, that passes an abstracted verification condition to the decision procedure, and lets the decision procedure say what it needs to complete the proof. If the solver finds a counterexample that depends on a function call, the summary of that function call is lazily encoded to a logical formula and incrementally passed to the solver, which continues the search. In effect, Calysto and Spear (the solver) incrementally inline functions as needed during the solving phase to avoid the potential exponential blowup that often happens if functions are inlined during the analysis (formula construction) phase.
Functions often have multiple side-effects. Sometimes, only one of those effects is relevant to the verification condition being proved, so Calysto slices each function summary with respect to function's side-effects, and inlines only the slice that's required by the solver to continue the proof.
Calysto features an interesting and effective proof localization strategy. I've found in practice that if there are any checks in code, those checks are frequently close to where the check matters. For instance, if a program dereferences a pointer, and the programmer wants to check that the pointer is not NULL, usually that check will be close to the dereference site. Thus, localization of proof can quickly discharge the proof obligation. For this reason, Calysto starts the proof from the assertion and goes backward in the call graph, adding additional constraints describing the callers' contexts, all the way until the main function, or until it proves the verification condition. I have measured ~200X speedups with this proof localization technique on the NTP server code.
Classical approaches to software verification either check each verification condition independently or try to prove them all at once (usually only for a single function). Calysto takes a new approach and tries to learn context-independent facts from each verification condition, so as to improve overall performance. My attempts in solving this problem have been moderately successful (see the STTT09 paper), and much more work remains to be done on this front.

Main Features

Calysto runs on Single Static Assignment (SSA) form, and as such is language independent. Only the rule files will need to be specified independently for each language-library combination.
Calysto is bit-precise, path-sensitive, context-sensitive, and field-sensitive (what I call *-sensitive).
Calysto currently handles loops and pointer arithmetic in an unsound manner, but that will change in the future, at least for some classes of loops. The basic framework is flexible enough to be extended.
Calysto exploits structure available in the software at several levels of granularity, which significantly improves the scalability.
Calysto is based on the LLVM compiler framework.
Calysto owns a lot of its scalability to close integration with Spear.

Calysto-generated Verification Conditions

Calysto-generated benchmarks are downloadable from the SMT-LIB and website, under Benchmarks, QF_BV category. Benchmarks are named Spear benchmarks, although, more accurately, they should have been named Calysto benchmarks. Using Spear and Spear tools, SMT-LIB benchmarks can be converted into various formats, like DIMACS CNF and Spear format. A more complete set of benchmarks is available on my old UBC website.

Availability

I'm not planning to make Calysto available. The focus of my research was on solving the technical problems, not on making the tool user friendly, so understanding the reports requires deep understanding of how the tool works. Thus, supporting the tool would be extremely time-demanding. With significantly more (engineering) work, this could have been solved in a more user-friendly manner. Also, I haven't been working on Calysto for quite a while, so it's out of sync with LLVM. While I was at Cadence, I was planning to make an improved production version of Calysto, but those plans were axed by the unfortunate downsizing.

If you want to find out more about Calysto, check out my thesis, the CAV07 structural abstraction paper, and the ICSE08 Calysto paper.

Acknowledgments

I'd like to thank numerous people that helped me during Calysto development and testing. Harlan Stenn from ISC provided incredibly quick and detailed feedback on the NTP bug reports that Calysto generated. Jesse Smith did the same for Bftpd. I also received feedback from numerous other developers, to which I'm all grateful.