PI: Stephen Kell, University of Kent

  • Much critical code continues to be written in C and other lower-level languages that include unsafe operations.
  • These can lead to security vulnerabilities. Existing approaches to gain assurance tend to be inflexible, targeting very specific scenarios.
  • This project seeks ways to increase flexibility, while retaining the accessibility and `explainability’ of dynamic tools.
  • We built a prototype tool built atop Frama-C and KLEE which can slice C code down to smaller programmes which are in some cases loop-free and therefore symbolically execute to termination.

Critical code continues to be written in C and other lower-level languages that include unsafe operations, such as unchecked array accesses and pointer casts, leading to security vulnerabilities. Many approaches exist for gaining assurance about these, but each is inflexible and target specific scenarios.

Static type-checking can be viewed as a program analysis that is baked into the host language design. Conversely, dynamic checking can be made `partially static’ by integrating it into a symbolic execution engine.

This project explored this continuum in search of a configurable program analysis of which traditional static type-checking is just one configuration. We framed the problem as seeking methods that would allow a relatively dynamic approach to become terminating, hence `static’, given the right program abstraction. Our insight is that program slicing offers such an abstraction; it retains or discards code based on a slicing criterion, which in our case is “Does this code affect whether the type assertions will pass”? For syntactically type-checkable programs, only a loop-free program should remain, roughly encoding “Might this raise a type error?”. Syntactic type assignments are loop-invariant by definition, and indeed this is how syntax-directed type-checking scales; in effect, we recover this fact during slicing, rather than enforcing it by construction in the language design.

We built a tool, Slice & Run, which encodes type-based properties as assertions which can be interpreted by the KLEE symbolic execution engine. Before feeding the program to KLEE, we apply a slicing-based abstraction whose goal is to recover a smaller version of the program whose exploration by KLEE terminates /in those cases that would also be statically type-checkable/, but is still (non-terminatingly) useful in those that would not. The tool is built using Frama-C and takes unmodified C code as input.

Besides considerable basic tool-building effort, the main challenge addressed in the 13 months of the project has been to accommodate patterns of polymorphic code. This requires careful design of the invariant protocol i.e. the rules for inserting assertions. This exercise mirrors the design of the language-level type-checking rules, but is separated from the base language, so can likely be applied largely independently of the source language. This contrasts with conventional type-checking innovations, whose benefits are conferred only on new source code written in new languages.

Symbolic execution is itself a technique offering a configurable depth of analysis, profiting from much complementary work. Meanwhile, it is likely that even programs that do not slice perfectly would benefit opportunistically from slicing, yielding greater coverage per unit time. Were the project able to continue, we would be exploring the benefits and practicalities around these approaches.

PUBLICATIONS. J. Adam, S. Kell. “Type checking beyond type checkers with Slice & Run. “TAPAS workshop at SPLASH 2020.