At INFILTRATE ’14 I gave a talk on the topic of fuzzing language interpreters. The slides are now available here. The results generated by the system presented and, subsequent, related work, were sufficiently good that my bottleneck quite soon moved from bug discovery to crash triage, which ended up forming the basis for my talk at INFILTRATE ’16.
The question addressed in the talk is ‘How can we fuzz stateful APIs in an efficient manner?’, where ‘efficient’ in this case means we want to reduce the number of wasted tests. For a stateful API, it’s probable that a given API call requires a preceding set of API calls to have set the environment into a particular state before it does anything ‘interesting’. If we don’t make an attempt to set up the environment correctly then we will likely end up with a lot of our tests discarded without exercising new functionality.
As you’ve probably guessed, and as I would assume many other people have concluded before me: a good source of such information is existing code written using the API. In particular, regression tests (and other test types) often provide self-contained examples of how to exercise a particular API call.
The talk itself is in two parts: firstly, a minimal system which works versus ‘easy’ targets, such as PHP and Ruby, and secondly, a more complex system which works versus more difficult targets, such as the JS interpreters found in web browsers.
Given that this talk was two years ago, the ideas in it have evolved somewhat and if you are interested in fuzzing either category of software mentioned above I would offer the following advice:
- For the easier targets, compile them with ASAN, extract the tests as mentioned and mutate them using something like radamsa. ASAN plus some batch scripts to automate execution and crash detection is sufficient to reproduce the results mentioned and also to find bugs in the latest versions of these interpreters. The system mentioned in the slides ended up being overkill for these targets.
On the topic of program analysis: if you are interested in learning about SMT-based analysis engines the early-bird rate for the public editions of ‘Advanced Tool Development with SMT Solvers’ is available for another week. The details, including a syllabus, are here, and if you are interested drop me an email via firstname.lastname@example.org.
Last week at Infiltrate I presented some early-stage work on crash triage under the title “Automated Root Cause Identification for Crashing Executions“. The slides can be found here, and the presentation notes contain further details in draft form.
A better title for this work would probably have been “Statistical Crash Triage” or possibly something involving the term “predicate synthesis“, as really those things are at the core of what was presented. The main algorithm can be summarised fairly quickly as follows:
- Run the target application on all the good inputs and all the bad inputs. Record coverage information.
- Use the coverage information to predict what functions are likely relevant to the crash.
- Rewrite those functions to insert instrumentation which will record all computed values and other properties.
- Rerun the instrumented version of the target application on all the good and bad inputs.
- From the recorded state, and predicate templates, synthesise and evaluate predicates over the program’s variables.
- Apply a lightweight statistical analysis to the evaluations of these predicates to shake out those relevant to the crash from those that are not.
The actual details are in the slides so I won’t go into that any further. The advantages of this approach are that it isn’t tuned towards one bug type, or class of applications, and simply relies on large amounts of input data and lightweight analyses to discover ‘interesting’ things. Alongside that, the analyses at each stage are parallelisable and so it’s quite simple to scale up. On a reasonably sized target (PHP) the approach is fast enough to fit into a normal workflow.
The most significant downside is that the generality means that if a bug is best described by a very complicated/precise predicate it may not be discovered (although more simple predicates may be, which can help a user manually discover the precise predicate more easily). In terms of the work as a whole there is also a weakness in the limited evaluation so far, but this is something I’m currently in the process of alleviating. In particular I’m working on testing with a wider variety of memory management issues as those pose some unique challenges for the algorithm above.
Besides the analysis algorithm itself, I also want to quickly mention CrashCorpus*. This is a corpus I’m currently working on for the evaluation of crash triage (and related) tools. A significant issue with the academic literature is that the algorithms tend to be tested almost exclusively on toy programs or synthetic bugs. The goal of CrashCorpus is to eliminate that by providing easy to build, easy to run, real-world targets. I’ll have more info on this once I get closer to a public release.
* I’m still building towards a public release of the corpus as it needs more targets before it is truly useful, but if you’d like to contribute drop me an email (sean _at_ vertex.re). All I require is a set of crashing inputs, a set of non-crashing inputs and the source code for the target. I’ll take care of the rest.
At WOOT’12 a paper co-written by Julien Vanegue, Rolf Rolles and I will be presented under the title “SMT Solvers for Sofware Security”. An up-to-date version can be found in the Articles/Presentation section of this site.
In short, the message of this paper is “SMT solvers are well capable of handling decision problems from security properties. However, specific problem domains usually require domain specific modeling approaches. Important limitations, challenges, and research opportunities remain in developing appropriate models for the three areas we discuss – vulnerability discovery, exploit development, and bypassing of copy protection”. The motivation for writing this paper is to discuss these limitations, why they exist, and hopefully encourage more work on the modeling and constraint generation sides of these problems.
A quick review of the publication lists from major academic conferences focused on software security will show a massive number of papers discussing solutions based on SMT technology. There is good reason for this 1) SMT-backed approaches such as symbolic/concolic execution have proved powerful tools on certain problems and 2) There are an increasing number of freely available frameworks.
The primary domain where SMT solvers have shone, in my opinion, is in the discovery of bugs related to unsafe integer arithmetic using symbolic/concolic execution. There’s a fairly obvious reason why this is the case; the quantifier free, fixed size, bitvector logic supported by SMT solvers provides direct support for the precise representation of arithmetic at the assembly level. In other words, one does not have to do an excessive amount of work when modeling the semantics of a program to produce a representation suitable for the detection of unsafe arithmetic. It suffices to perform a near direct translation from the executed instructions to the primitives provided by SMT solvers.
The exploit generation part of the paper deals with what happens when one takes the technology for solving the above problem and applies it to a new problem domain. In particular, a new domain in which the model produced simply by tracking transformations and constraints on input data no longer contains enough data to inform a solution. For example, in the case of exploit generation, models that do not account for things like the relationship between user input and memory layout. Obviously enough, when reasoning about a formula produced from such a model a solver cannot account for information not present. Thus, no amount of computational capacity or solver improvement can produce an effective solution.
SMT solvers are powerful tools and symbolic/concolic execution can be an effective technique. However, one thing I’ve learned over the past few years is that they don’t remove the obligation and effort required to accurately model the problem you’re trying to solve. You can throw generic symbolic execution frameworks at a problem but if you’re interested in anything more complex than low level arithmetic relationships you’ve got work to do!
The slides for most of the talks from this years Infiltrate have gone online! Among them you can find the slide deck for Attacking the WebKit Heap, which Agustin and I gave.
The talks were awesome and I’d recommend grabbing them all. Halvar’s, titled State Spaces and Exploitation, was one of my favourites. I generally believe that the reason we in industry, as well as university based research groups, sometimes fail to build better tools is because we don’t spend enough time reflecting on the nature of exploitation and bug finding and as a result end up solving the wrong problems. Halvar spent about half of his talk addressing one way to think about exploits, which is programming a ‘weird machine’ that lives inside a program and is unlocked by a bug trigger. It’s an interesting way to look at things and, as he mentioned, similar to how many of us think of exploit development when it comes down to it.
As far as I know, we’ll only be releasing audio for one of the talks, Nico’s keynote on Strategic Surprise, which can be found here. Also worth checking out, educational, funny and just a little bit troll-y … what more can you ask =D
“We don’t care about nulls because this ain’t no strcpy shit” – Ryan Austin, by consensus the best quote of the conference.
Ruxcon is next month and I’ll be giving a talk titled Code Analysis Carpentry (Or how not to brain yourself when handed an SMT solving hammer). Here’s the abstract:
This talk will be one part “Oh look what we can do when we have a Python API for converting code into equations and solving them” and one part “Here’s why the world falls apart when we try to attack every problem in this way”.
One popular method of automated reasoning in the past few years has been to build equational representations of code paths and then using an SMT solver resolve queries about their semantics. In this talk we will look at a number of problems that seem amenable to this type of analysis, including finding ROP gadgets, discovering variable ranges, searching for bugs resulting from arithmetic flaws, filtering valid paths, generating program inputs to trigger code and so on.
At their core many of these problems appear similar when looked at down the barrel of an SMT solver. On closer examination certain quirks divide them into those which are perfectly suited to such an approach and those that have to be beaten into submission, often with only a certain subset of the problem being solvable. Our goal will be to discover what problem attributes place them in each class by walking through implemented solutions for many of the tasks. Along the way the capabilities and limitations of the modern crop of SMT solvers will become apparent. We will conclude by mentioning some other techniques from static analysis that can be used alongside a SMT solver to complement it’s capabilities and alleviate some of the difficulties encountered.
The schedule is full of talks that look like fun. I’m really looking forward to seeing a few in particular, especially those by Silvio Cesare, Ben Nagy and kuza55. Looks like it’ll be just as entertaining as REcon (with hopefully not quite as much sun-burn)! Mostly I’m just looking forward to watching 30 people get on stage and try to out do each other with sheep related innuendo. If there isn’t at least one drunken presenter abusing the crowd I’m calling it a failure!
Last week I spoke at REcon on the above topic. The slides can be found here. The abstract for this talk is as follows:
As reverse engineers and exploit writers we spend much of our time trying to illuminate the relationships between input data, executed paths and the values we see in memory/registers at a later point. This work can often be tedious, especially in the presence of extensive arithmetic/logical modification of input data and complex conditions.
Using recent (and not so recent) advances in run-time instrumentation we can go a long way towards automating the process of tracking input data and its effects on execution. In this talk we will discuss possible approaches to solving this problem through taint analysis. The solutions we will discuss are useful in many scenarios e.g. determining the set of conditional jumps under our control, discovering buffers in memory that are useful for injecting shellcode, tracking parameters to potentially insecure function calls, discovering ‘bad bytes’ for exploits and so on.
Building on this we will delve into the construction of logical formulae expressing the relationships between input and data in memory and ways in which these formulae can be manipulated and solved for interesting results. Depending on how we manipulate the initial formulae we can use theorem provers to automatically solve many problems e.g. ‘unraveling’ arithmetic/logical modifications on input, generating inputs that trigger specific paths, discovering the bounds on given variables and so forth.
I will update this post whenever the REcon videos etc go online. In the meantime I should probably finish at least one of the 5 or so blog posts in a semi-complete state 😛
I got back from the latest ISSA Ireland seminar today. The event was held in Dublin and consisted of a number of talks and a panel discussion. There was an excellent crowd and some really interesting people with conversation varying from program analysis to governmental cyber-security policy.
I gave a presentation titled ‘VoIP Security: Implementation and Protocol Problems‘ which was a relatively high level talk about finding bugs in VoIP applications and deployments. It consisted of an overview on finding vulnerabilities in VoIP stack implementations and auxiliary services and introduced some of the common tools and methods for discovery/enumeration/attacking VoIP deployments.
Hart Rossman, of SAIC, gave an excellent talk which touched on a number of different issues around developing and implementing cyber-defence policies. Aidan Lynch, of Ernst and Young, discussed security issues in deploying VoIP in a corporate environment. The panel discussion focused on securing national infrastructure (or so I’m told because I managed to miss that). And finally there were a number of lightning talks; of particular interest was one on the application security process in Dell which introduced me to the concept of threat modelling and Microsofts TAM tool. (There is an MSDN blog here which contains a lot of good information on the topic in general)
It was an educational day all round and I’d like to thank the organisers for inviting me to present and being such excellent hosts.