Day 5

Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)

Armando started his talk by demonstrating the automatic synthesis of a program for swapping two integer variables without using a third. It’s a standard algorithm and quite small but was still cool to see. He then demonstrated a few more algorithms involving bit-level arithmetic. The implementation of this tool, called Sketch, can be found here. The demonstrations given were for a C-like language and apparently synthesis works quite well for algorithms based around bit-twiddling.

These programs were generated from program ‘sketches’, essentially algorithmic skeletons, and a test harness, similar to unit tests, that described the desired semantics of the program. The sketches express the high level structure of the program and then the details are synthesized using a SAT solver and a refinement loop driven by the tests. The idea of the sketches is to make the problem tractable. The intuition for this was given by the example of curve fitting. That can be a difficult problem if you have nothing to go on but data points whereas if you are told the curve is Gaussian, for example, the problem becomes much more feasible.

The synthesis algorithm first uses the sketched fragment to generate a candidate program and then a SAT solver is invoked to see if the conjunction of this program and the semantics described by the tests are valid. If not, a counter-example is generated and used to refine the next iteration of program generation. This is incredibly simplified and the full details can be found in Armando’s thesis.

This was yet another talk where there was an emphasis on pre-processing formulae before they get to the solver. The phrase ‘aggressive simplification’ was used over and over throughout the conference and for synthesis this involved dataflow analysis and expression reduction (e.g. y AND 1 reduces to y) as well as more standard common sub-expression elimination.

Day 6

Harnessing SMT power using the verification engine Boogie (Rustan Leino)

This talk began with some coding demonstrations in a language called Dafny that has support for function pre-conditions, post-conditions and loop invariants. As these features are added to a code-base they are checked in real time. Dafny is translated into an intermediate verification language (IVL) called Boogie (the verification system for it is open source under the MS public license) which can be converted into SMT form and then checked using the Z3 SMT solver. While this fun to watch, most languages don’t have these inbuilt constructs for pre/post-conditions and invariants. Fortunately, Boogie is designed to be a generic IVL and translation tools exist for C, C++, C#, x86 and a variety of other languages (although from what I gather only some of these are publicly available and none are open source). As such, Boogie is designed to separate the verification of programs in a given language from the effort of converting them into a form that is amenable to checking.

The high level, take-away message from this talk was “Don’t go directly to the SMT solver”. It relates to the separation of concerns I just mentioned. This lets you share infrastructure and code for verification tasks that will be common between many languages and also means you have an intermediate form to perform simplification on before passing any formulae to a solver.

HAVOC: SMT solvers for precise and scalable reasoning of programs (Shuvendu Lahiri & Shaz Qadeer)

HAVOC is one such verification tool for C that makes use of Boogie. It adds support for user-defined contracts on C code that can then be checked. Based on the Houdini algorithm HAVOC can also perform contract inference with the aim of alleviating much of the burden on the user.

I really wish we had something similar to HAVOC for code auditing (this was actually one of the use cases mentioned during the talk). I’m not sure about others but essentially how I audit source code involves manually coming up with pre-conditions, post-conditions and invariants and then trying to verify these across the entire code-base by hand. This is fine, but with a tool-set of vim, ctags and cscope it’s also incredibly manual and seems like something that could at least be partially automated. It was mentioned that a more up-to-date version of HAVOC might be released soon so maybe this will be a possibility.

Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes)

This talk was on probabilistic approaches to SAT solving. These techniques still lag far behind DPLL based algorithms on industrial benchmarks but are apparently quite good on random instances with large numbers of variables.

Symbolic Execution and Automated Exploit Generation (David Brumley)

While I previously ranted about the paper this talk was based on, this talk was a far better portrayal of the research. Effectively, we’re in the very, very early stages of exploit generation research; while there have been some cool demos of how solvers might come into play we’re still targeting the most basic of vulnerabilities and in toy environments. All research has to start somewhere though, my own thesis was no more advanced, so it was good to see this presented with an honest reflection on how much work is left.

One interesting feature of the CMU work is preconditioned symbolic execution which adds preconditions to paths that must be satisfied for the path to be explored. This is a feature missing from KLEE but would be just as useful in symbolic execution for bug finding as well as exploit generation. Something that remains to be researched and discussed is efficient ways to come up with these pre-conditions.

Conclusion

The summer school was a great event and renewed my enthusiasm for formal methods as a feasible and cost effective basis for bug finding and exploit development. The best talks were those that presented an idea, gave extensive, concrete data to back it up and explained the core concepts and limitations with real world examples. I hope to see more papers and talks like this in the future.

A generic conclusion for the six days would be difficult, so instead the following were the reoccurring themes that stood out to me across the talks that may be relevant to someone implementing these systems:

– Focus on one thing and do it well. For example, separate instrumentation from symbolic execution from solving formulae.
– Aggressively simplify before invoking a solver. Simplification strategies varied from domain specific e.g. data-flow analysis, to generic logical reductions but all of them greatly reduced the complexity of the problems that solvers had to deal with and thus increased the problems the tools could handle.
– Abstract, refine and repeat. The concept of a counter-example guided abstraction refinement loop seemed to be core to algorithms from hardware model checking, to program synthesis, to bug finding. In each, CEGAR was used to scale algorithms to more complex and more numerous problems by abstracting complexity and then reintroducing it as necessary.
– Nothing beats hard data for justifying conclusions and driving new research. This point was made in the earliest talks on comparing SAT solver algorithms and reiterated through the SAGAN information collection/organisation system of SAGE. Designing up front to gather data lets you know where things are going wrong, keeps a record of improvements and makes for some pretty cool slides when you need to convince other people you’re not insane =)

The slides for the summer school have started to go online so for the remaining days I’ll just give a quick summary of parts I thought were particularly interesting or comments that were made but not in the slides.

Day 3

BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena)

The first thing of note from this talk was a brief discussion on selecting paths for analysis during symbolic/concrete execution. Anyone who has used KLEE knows the lack of sane path selection mechanisms is a significant drawback so it was good to see one of the talks on this type of system discuss it. The methods used were dataflow and control flow distances to functions of interest.

An interesting problem tackled later in the talk was how to distinguish due from undue influence of tainted data over control flow. For example, it might be acceptable for user data to taint a value used in a switch statement that selects a function to run but it’s unlikely to be very good if it can taint a function pointer directly. Four different methods were presented from distinguishing these cases, the simplest being point by point exhaustion using a solver of the number of possible target addresses in the address space. More complex probabilistic and information theoretic approaches were also discussed and are elaborated on in their paper. It would be nice to see some more experimental data with these more advanced methods though as it is limited to 3 vulnerabilities and 3 benign cases.

SAT-based Model-Checking (Armin Biere)

Armin is the developer of one of the best SAT solvers, Lingeling, and his talk discussed advances in using SAT technology for model checking. During the talk he mentioned a paper by Aaron Bradley on SAT based model checking without unrolling which might be worth checking out but I haven’t had a chance to yet

CryptoMiniSat — A Rough Guide (Mate Soos)

This was a great talk by Mate Soos on CryptoMiniSat, which won last years SAT Race and is open source, and SAT solver design. Mate started with a discussion of the software design philosophy behind the project and put forward that it’s better to have less optimised and complex code if you can more easily implement better ideas. Given that his solver is faster than Lingeling, which is far more difficult to comprehend, it seems that he is correct. He had some other interest things to say on SAT solver features, emphasising regular simplification of expressions and maintaining a cache of results from unit propagation even if they are not currently useful.

SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar)

In my opinion, this was the best talk of the summer school so far. Patrice and David discussed SAGE and presented a lot of data to encourage the development of tools for this kind of testing. SAGE is built on top of previously developed MS tools detecting crashes (AppVerifier), recording traces (Nirvana), generating constraints (TruScan) and solving constraints (Z3).

Unlike KLEE and the Bitblaze tools, the symbolic execution part of SAGE only accounts for a small fraction of the time cost. Only 1/4 of the total time is spent on symbolic execution with the remainder of their 3 week fuzzing runs spent on tracing, generating constraints and running the application under test on the fuzz files.

One interesting thing mentioned was that while most queries to the solver only take 1/10th of a second all queries are capped at 5 seconds and after that the solver is killed and the result is presumed UNSAT. This is based on the observation that they get more code coverage by this method than waiting for hours for a single query to return. They backed this up with some statistics that showing that longer run times only very rarely led to more bugs.

Some other points of note were:
– From the start SAGE was engineered to provide enough information and statistics on every part of its system that determining what it is doing and where it is succeeding/failing is possible. This is facilitated through a system called SAGAN that allows them to focus on areas needing work.
– SAGE is primarily deployed against file parsers. This is a use case where the majority of non-determinism is from the input. In other environments with different sources of non-determinism it might be more difficult to direct the application through constraint solving.
– Most OOM conditions are a result of trying to store the constraints in memory while analysing the trace, not in the solver as I would have expected. As a result, simplification and expression elimination can be necessary even before that staged.
– Most crashes seemed to be concentrated within the first 6 generations of constructed fuzz files but crashes were seen in all generations up to the mid to late teens. I don’t think they’ve ran for any longer than that.
– SAGE was responsible for 30% of bugs found in a certain class of file parsers on Windows 7. These were bugs missed by all other testing mechanisms. I wonder how long it will be before those of us interested in bug finding will have to start looking at tools like SAGE from the point of view of discovering where they are weak as a starting point for auditing.

All in all, this presentation had hard data to support some very exciting conclusions.

Day 4

Approaches to Parallel SAT Solving (Youssef Hamadi)
I had recently been wondering what the state of the art in parallel solving is so this was good to see. Youssef first started by proposing that we are unlikely to see order of magnitude speed ups in SAT solving based on advances in the current CDCL architecture of SAT solvers. I guess there are two ways to deal with this, one is to look at different approaches to sequential SAT solving and the other is to look at parallelism.

From 1996 to 2008 most of the approaches to parallel SAT proceeded by splitting the problem space into chunks and solving these instances in parallel with clause sharing of clauses under a certain size. Another approach is the portfolio approach used by parallel Z3, PLingeling and ManySAT. In this approach the same problem is attacked by several different solver instances each using a different configuration. The solver configuration is parameterized on the restart policy, polarity selection, clause learning and branching heuristics. This lead to super-linear speed-up with combinations of these solvers performing better than the sum of their parts.

One particular issue for this strategy though is how best to do clause sharing between solvers. Sharing of large clauses can be costly so one needs a strategy to figure out the upper limit on the size of clauses to share. This is complicated by the fact that the size of learned clauses progresses as the solver advances in the problem. Two algorithms were discussed in this context. The first was based on TCP bandwidth calculation algorithms that slowly increase the size of shared clauses and then quickly back off once a problem is detected and a heuristic based on variable activity to set a quality threshold on clauses to accept from other solvers.

This portfolio mechanism works well for between 4 and 8 cores but after that the effects of added cores is greatly diminished.

SAT Solving and Complexity Theory (Ryan Williams)

This was a theoretical talk that discussed some of the difficulties that people have ran into in not only proving P != NP but on many problems on the relations between complexity spaces. Much like the talk by Shai Ben David I’m pretty sure I’d butcher the mathematical details were I to summarise but the take away message was similar: the logics for reasoning and proof techniques that we have today for problems like this are quite insufficient; as a result people have struggled to even do far weaker reasoning like establishing lower bounds on NP-complete problems. It was a really interesting talk but I’ll definitely need to rewatch the video when it comes out =D

Independence Results for the P vs. NP Question (Shai Ben David)

This was a really fun talk that was very much on the theoretical side of logic and satisfiability but with potentially very important implications. Ever since learning about early 20th century work by Hilbert, Godel, Turing etc. on foundations of logical systems and proofs I’ve been fascinated by anything that discusses the universal limitations and capabilities of logical systems. This was the first talk I’ve seen where this kind of purely theoretical work was linked to an implication for solving technologies. The fundamental question approached in the talk was whether P != NP is an irresolvable question give the logics we have available. That is, can we prove that it is unprovable.

I would do it injustice to try and summarise the talk (and I’d get it wrong!) but the main result was that if it were true that P is nearly equal to NP then we would not be able to prove P != NP using current lines of reasoning and tools. The interesting result for SAT solvers is that if this were the case then many of the problems we want to solve may be solvable in almost-polynomial time. The downside is that even if we could prove this the proof probably wouldn’t help at all in building a solver than can exploit this closeness.

I’ve totally butchered the details of this talk but you can find a earlier/shorter version of it here and a paper here.

HAMPI: A Solver for String Theories (Vijay Ganesh)

Vijay’s talk was on the HAMPI solver. HAMPI contains a theory for bounded (that’s important) character strings that allows it to reason about things like whether a regular expression matches against a particular string or not. From what I gathered, it operates by converting a regular expression into a context-free-grammar and then converting that context-free-grammar, along with any constraints we may wish to check, into a formula over bitvectors and checking the satisfiability of this with STP. The main target application was detecting oversights in regexs designed to catch SQL injection attempts but Vijay also mentioned they got a 2-5x speed-up when using this solver with KLEE on applications that do a lot of string manipulation. KLEE tends to perform quite poorly on things like XML parsers so I’d love to see if specialised solvers can help out here.

Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)

This was a good talk by some of the best guys building SMT solvers, Leonardo De Moura and Nikolaj Bjorner. Both of their publication pages are worth checking out for details on building SMT solvers as well as the theoretical aspects.

They first highlighted some of the core problems in SMT solvers that affect performance: combining engines, unfairness between theory solvers and quantifiers. The most interesting part of the talk for me was on the use of abstraction/relaxing and then refinement when dealing with complex problems. For example, abstracting problems problems using uninterpreted functions and then checking satisfiability may reduce the complexity of the original problem. If it turns out that is UNSAT then the original is UNSAT and if you get a SAT result you can then refine the abstraction if necessary and check again. This idea of abstraction/refinement (CEGAR I guess) loops came up a lot in many different talks.

Also interesting was the mention of their verifying compiler projects that do function level verification and use contracts for called functions in the analysis rather than analysing down into them. I know the idea of contracts is used in HAVOC and discussed extensively in Thomas Ball’s publications but I’m not sure if this was the project they were referring too.

Scalable Testing/Reverse Engineering/Performance Profiling with Parallel and Selective Symbolic Execution (George Candea & Stefan Bucur)

The next talk was on the guys behind S2E and Cloud9. Cloud9 is cool in that it’s a big cluster of nodes each exploring different parts of a tree in symbolic execution. They found run times for gaining a particular code coverage percentile to drop dramatically when going from 1 to 8 nodes and then drop even further as they went up to 48 nodes. The total effect being a drop from 6 hours to minutes for the particular example.

S2E caught my attention a few weeks ago after reading their paper as it is designed to be a platform for writing analysis tools that leverage symbolic execution. To my knowledge it is the first system of this kind that allows a callback/event based mechanism for analysis tools and can target an entire operating system stack (it’s built on QEMU). They have some good documentation as well which is crucial for getting users involved. When I grabbed the code a few weeks back I did notice some dramatic slowdown in execution times even when not doing symbolic execution so that’s an issue that will have to be addressed but this looks like it could be a great project. With the combination of docs and well thought out design I’m hoping for the PIN of symbolic execution tools.

In the later part of their talk they gave some feedback to the SMT developer community with suggestions for improvements. For example, 30% of the time spent within their solver (STP) was spent in memory allocation routines. It’s something I haven’t seen a whole lot written on but the type of work that SMT engines is probably specific enough to require carefully crafted memory allocation algorithms. It’ll be interesting to see what comes of this in the future.

CVC3 and Applications (Clark Barrett)

Clark Barrett has been involved in SMT solver development for probably as long as anyone else and as CVC3 is the solver used internally in Immunity Debugger this talk was of particular interest. Clark mentioned that CVC4 is in development and should be seeing a release sometime this year so that’s good news. We’ve had some issues with CVC3 dealing with large array constraints and as this is being redone it should hopefully fare a bit better.

Unrelated to CVC3 really but one of the comments at the end was kind of striking in that the person said they often found using the theory of linear integer arithmetic with constraints to represent the bounded nature of 32-bit values faster than the theory of bitvectors. I guess that has something to do with their application area and the kinds of constraints if they’re not heavy on bit-level operations but it was something I’ve never thought to do before.

CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)

Karem Sakallah was one of the most entertaining speakers of the day and also presented some interesting ideas behind a verification system based on model checking and Counter Example Guided Abstraction Refinement (CEGAR) that is currently being used to verify real hardware. This was the second talk of the day in which abstraction and refinement using uninterpreted functions were discussed to make difficult problems more tractable (the first being the one by the MSR guys). In this talk Karem also mentioned that naive refinement was not sufficient. So, typically what happens is that when a SAT result turns out to be a false positive a constraint is generated that will block that result from being given again and this is added to the global state. To alleviate this some post-processing is done on the generated formula. They weaken the conditions so that it entails an entire family of states. For example, if the condition was (a == 5 AND b == 6) they weaken it to (a < b). I have no idea how they prevent this weakening from excluding valid states so I’ll need to follow up on that tomorrow =D

A final point made was that throughout their development process they built a number of optimisations but discovering the best combination of these optimisations was a trial/error process. The graph shown for this varied from combinations of optimisations that had no effect at all to some that cut the execution time to minuscule fractions of the base case.

This week I’m attending the first SAT/SMT Summer School, organised by Vijay Ganesh and hosted at MIT. There are plenty of interesting talks, organised into three categories, so I figured it might be useful to do a brief summary of each day with some links to relevant material. I’ll update this post as the week progresses.

Introduction to Satisfiability Solving with Practical Applications (Niklas Een)

The first day of talks was a preliminary day, providing introductions to the foundations of the SAT and SMT problems and a quick history of how the research areas have progressed. Niklas Een, one of the MiniSAT developers, opened the technical part of the conference discussing the history of automated approaches to SAT. He then moved on to an overview of the algorithms that form the core of most SAT solvers. In Niklas’ opinion the most important algorithms in terms of their impact on the ability of SAT solvers have been those for conflict clause analysis and variable activity tracking. Perhaps an obvious point, but one worth making was that often industrial SAT problems are trivial once you know what part of the graph to explore and hence why algorithms for locating this are quite important. One idea that was reiterated multiple times was that the development of SAT solvers is largely an experimental science and that even though we can give intuitions as to why certain algorithms are useful, in many cases nobody has a clue what the true reason is, not even the algorithms inventors.

SMT Theory and DPLL(T) (Albert Oliveras)

The second talk was by Albert Oliveras and provided an introduction to SMT solving. After a quick discussion on the motivation for SMT solvers Albert gave an overview of both the lazy and eager approaches to SMT solving. The eager approach, embodied in solvers like STP, involves directly encoding the expressions over different theories into a SAT problem and then using a SAT solver on that problem. The lazy approach, found in Z3 among others, has two distinct systems – a SAT solver and one or more theory specific solvers, and proceeds by finding SAT solutions to a propositional skeleton and using theory specific solvers to check for consistency of the returned model in their domains. Albert also provided a good high level summary of how these theory specific solvers share information. The slides from this talk can be found here and are definitely worth a look for an introduction to the topic.

SAT Solvers for Formal Verification (Ed Clarke)

After lunch Ed Clarke continued the introductions with a basic summary of bounded model checking (BMC) and linear temporal logic (LTL). BMC has progressed over the years from initially using basic data structures to explicitly represent states to the use of binary decision diagrams and on to SAT encodings. Its an interesting topic and there are many parallels and cross overs between modern versions of these algorithms (and CEGAR) and symbolic execution based approaches to verification. The second part of Ed’s talk was on current research his students are doing into the use of bounded model on systems that have properties modelled by differential equations. I apparently didn’t pay enough attention in calculus classes because most of this went over my head =) The work is being led by Sicun Gao so if you’re interested his research page is probably helpful.

SMT-LIB Initiative (Cesare Tinelli)

Following this, Cesare Tinelli talked about the SMT-LIB and SMT-COMP initiatives. It was interesting to hear the story behind how it started. One thing of note that Cesare said is that back when this was started it was incredibly hard to tell what algorithms and extensions to SAT solvers were truly useful. This was because of unstandardised reporting and also because the tendency of developers to report on the benchmarks that their tools performed particularly well on. This is relevant I think because we are at a similar stage with symbolic execution and security focused tools. It’s hard to tell what really works as sometimes the tools aren’t released and when they are it can be quite difficult to recreate the authors results. It might be useful for some sort of standardised benchmark/testing suite with a focus on modern problems, especially as people move into other areas like automatic exploit generation.

An interesting discussion broke out near the end on the usefulness of the SMT-LIB standard as an input mechanism for tools given that it is not designed for efficient storage and so writing large problems to disk to read into a solver isn’t feasible for many cases in symbolic execution. The solution here seems to be to simply embed a solver and use its C/OCaml/etc API but that does somewhat nullify the usefulness of the SMT-LIB language as anything more than a standard and teaching tool. It might be interesting to see a version of the language developed specifically with the goal of efficient storage and parsing though.

Constraint Solving Challenges in Dynamic Symbolic Execution (Cristian Cadar)

The final talk of the day was by Christian Cadar on the technologies behind EXE and KLEE, with a focus on the problems of solving the types of constraints generated. Using the example of constraints over arrays, Christian made the point that it can be useful to modify a solvers algorithms for a particular theory for domain specific cases. The graph presented showed a reduction from something near exponential slowdown to linear slowdown by removing the array axioms typically added for every array based operation (and one other thing that escapes me right now!) and thus checking an under-approximation of the original formula.

These tools are essentially mixed symbolic/concrete execution tools with a focus on bug finding, equivalence checking and so forth. KLEE is open source, which is a definite plus and worth checking out. I’d love to hear some feedback from people on its performance as I’ve ran it a few times and haven’t really gotten results that are as useful as fuzzing or manual auditing for bug finding. I think for tools such as this a large set of standardised benchmarks in modern applications could be very useful for gauging progress and focusing research efforts. Apparently Microsoft Research have found this approach very useful in their SAGE framework but it’s hard to tell if it can be used generally when you don’t have a data-center and a dedicated research group.

And that was it! Fun day and tomorrow looks awesome =)