Summary: This post explains why security research is relevant for this blog, and discusses three specific areas worth tracking.
Hi folks – I’m back (vacations and all that).
Security people deal with finding security issues (vulnerabilities) in systems. This blog deals with a different topic: big-system verification, where verification is defined as finding functional / safety / performance bugs.
However, security research and practice are pretty relevant for big-system verification: The two topics are related, and share many techniques and methodologies.
Also, for better or worse, security is hot now. So it receives a lot of funding and mindshare, which means that we (verification folks) can gain by tracking what works for security, and trying to translate it into our domain.
I’d like to discuss here three specific areas in security research (out of many) which I think we should keep an eye on:
- Fuzzing, in general, is similar to CDV, and thus really relevant
- Instantiating attack patterns is similar to the problem of instantiating hazard patterns
- Trying to do more with fewer notations is a big issue in both security and verification
More on each of these areas below.
Fuzzing
Fuzzing, or fuzz testing, is a technique for finding bugs (mainly security vulnerabilities) in SW (or HW). It involves bombarding the SW with random, almost-legal inputs, with the hope of causing it to crash in various ways, or otherwise do something which exposes a vulnerability which the bad guys can use.
As the Wikipedia page explains, there are two main kinds: mutation-based fuzzing (where you take legal inputs and mutate them in various interesting ways), and generation-based fuzzing (where you build almost-legal inputs from some declarative description, e.g. a grammar). AFL is a really good (and free) mutation-based fuzzer.
Fuzzing (especially generation-based fuzzing) is a lot like CDV: It involves randomizing input according to constraints / structure, and (for the better ones like AFL) keeping coverage metrics, trying to auto-fill coverage, automatic failure clustering and so on.
I have mentioned fuzzing before in FV has much better PR than CDV, and said:
Even in security, most of the security holes which are found “by machine” (by either the good guys or the bad guys) are found via a technique called fuzzing. And “fuzzing” is roughly “the name security people gave to CDV”. For instance, check out the excellent, free AFL.
There is a new post by Michal Zalewski, the guy who wrote AFL (and whose judgement I tend to trust): Understanding the process of finding serious vulns. It is a preliminary review of his attempt to gather statistics about how people actually find high-impact vulnerabilities. The first point of his summary says:
The use of fuzzers is ubiquitous (incidentally, of named projects, afl-fuzz leads the fray so far); the use of other automated tools, such as static analysis frameworks or concolic execution, appears to be unheard of – despite the undivided attention that such methods receive in academic settings.
This seems consistent with my view on the topic (expressed in my post mentioned above): static / formal techniques are good, but most bugs are found via disciplined, metric-based, smart random testing – a fact that would be lost on you if you only read academic papers.
Instantiating danger patterns
One of the big challenges in big-system verification is that it is not enough to just combine randomly known basic events, however smartly: Because these systems interact with the wild, open world, you are bound to completely miss some basic dangers unless you explicitly model them (like that bridge-to-Malmo story).
In the post about spec bugs (just before the last chapter) I talked about one possible solution: instantiating “generic hazard patterns”. I said:
Developing a taxonomy of such generic hazard patterns, and applying it to the system-at-hand where applicable (with some user help) may be one way of tackling the “how do you even dream up new basic events” issue mentioned here.
Security, of course, has a similar problem – how to dream up all the attack kinds the bad guys might do. And – lo and behold – they actually have catalogs of generic “attack patterns”, e.g. the Common attack pattern enumeration and classification.
This is a list of patterns, each of which may or may not be relevant for a specific design. And people have done work on the instantiation problem. For instance, A Security Verification Framework for SysML Activity Diagrams (full disclosure: I did not read all 141 pages) describes a system in which you:
- Convert (manually) the various attack patterns into activity diagrams
- Describe the user design also as an activity diagram
- Connect the two and try to find if such an attack is possible, and at what probability (using Prism, a probabilistic model checker)
Doing more with fewer notations
One of the main things which helped push CDV along was the invention of the Hardware Verification Language (HVL), which was sort-of able to describe everything which HW verification needs: Generation of both data and sequences, coverage collection, checking and so on. Once such a language exists, you suddenly have a standard flow of doing things: You can later improve/refine the various engines and methodologies, but you have a starting point.
Neither big-system verification nor security seem to have that, and thus both seem to suffer from the curse of “10k languages feeding 100k tools”: They are very splintered, and there is no continuum to build on.
For instance, in safety (which is a big part of big-system verification) there is the useful, standard notation of fault trees. They essentially describe an and/or tree of “things which could go wrong”, together with their known failure probabilities (there is also a sequencing node, called “priority and”). Given such a tree, you can compute the failure probability of the root of the tree (signifying e.g. “airplane falls out of the sky”) and check that it is no more than, say, once in 10**9 hours.
This is a good notation, but it is too simplistic:
- Fault trees are a good way to reason about the probabilities of problems we understand very well, but (by definition) we don’t understand bugs until we have captured them.
- Thus, fault trees don’t really work for SW: All attempts to compute “the failure probability for a piece of SW” are somewhat pathetic – e.g. the Ariane 5 bug was just sitting there waiting for the maiden flight (with a probability of 1), but fault-tree analysis was completely irrelevant for it.
So fault trees are very good at what they do, but are not enough. So ideally we should be able to invent a notation which (among other things) includes fault trees, or can be easily translated to and from fault trees.
Such a well-accepted invention has not come forward yet, though there are some valiant tries. For instance, Causality checking of safety-critical software and systems (also long) describes a way to define a system via UML/SysML diagrams (plus probabilistic assertions). The corresponding bugs (found, again, via probabilistic model checking) are transformed into the fault-tree notation for easy understanding.
Security has similar issues. In fact, attack trees (and attack-defense trees, which also include countermeasures) are the security world’s parallel of fault trees. And just like fault trees, attack trees are good but too simplistic, and don’t (in general) play well with other notations.
Many other notations are used for modeling security concerns. For instance, the above-mentioned A Security Verification Framework for SysML Activity Diagrams uses (duh) activity diagrams as input. They talk about attack trees as an alternative, un-connected notation.
I would expect security research and practice to eventually come up with some unifying notations (anybody knows of any?) – this would be interesting to track.
BTW, on a completely different front, Facebook just externalized GraphQL – a unifying language and framework for accessing data, which is higher level than SQL, works for SQL / NoSQL / whatever databases, allows query verification, and so on.
Notes
I’d like to thank Sandeep Desai and Amiram Yehudai for reviewing a previous draft of this post.