Lightweight Static Guarantees
Time: 13:30 - 14:30
Room: Collegeruimte Ruppert C
Speaker: Oleg Kiselyov and Chung-chieh Shan
Title: Lightweight Static Guarantees (aka: eliminating array bound checking without dependent types)
We have identified a disciplined programming style that uses existing type systems in practical, mature languages to statically verify safety properties and make software more reliable and efficient. Because this technique requires no new language, extension or tool, it is easy to adopt to new application domains. The technique is compatible with imperative code, native mutable arrays, indirect indexing, and general recursion. The technique uses existing facilities for type abstraction and generic programming to express a wide range of safety properties as types. For example, we are able to statically eliminate most or all null pointer (empty list) and array bound checks.
We rely on an old idea of enforcing invariants via an abstract data type. The value of an abstract data type represents a capability; the small code that builds such values is a (domain-specific) trusted kernel. The type checker then enforces authorization of capability-based operations and thus extends trust from the kernel to the rest of the program. Parametric polymorphism available in modern languages lets us express many more safety properties, by using types as proxies for values. The problem of verifying the whole program can hence be reduced to that of verifying a compact trusted kernel.
The notion of the trusted kernel also applies to expressive type systems such as that of Haskell. This lets us statically assure the safety of low-level code, e.g., that accessing a memory region through a pointer respects properties of the region such as its size, alignment, endianness, and write permissions---even when allowing
pointer arithmetic and casts.
In an industrial setting, we are applying this approach to our own programs, such as Web application servers. We are also popularizing this discipline by concrete case studies, and welcome suggestions of new areas and examples.
More information, including the complete code, is available from: