Lightweight Static Guarantees Oleg Kiselyov and Chung-chieh Shan 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 uses existing facilities for type abstraction and generic programming to express a wide range of safety properties as types. These properties include: - never dereferencing a null pointer; - always sanitizing user input in database commands; - accessing an array using only indices that are in bounds; - performing modular arithmetic in cryptography using a consistent modulus; and - releasing all acquired resources such as locks, exactly once. Because this technique takes advantage of type systems that programmers already know and use today, it is easier to adopt and less invasive on an existing code base or development process, compared to a new language or an external checker. A developer can add new domain-specific safety properties to be checked, even before formalizing their mathematical foundation. The resulting program is not just more reliable but also more efficient, because fewer run-time checks are needed. 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. The basic idea behind our programming style is simple and old: enforcing invariants by using an abstract data type. The value of an abstract data type represents a capability; the small code that builds such values is a 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. In other words, we state safety properties in the type language, and the type checker enforces them during compilation. It turns out that the facilities for generic programming (parametric polymorphism) in modern languages let us express many more safety properties, by using types as proxies for values. The simplest case is to assure the safety of partial operations, where allowed values are known at compile time. This case includes - dereferencing only non-null pointers; - dividing by only non-zero denominators; - taking the head or tail of only non-empty linked lists; - indexing into a static buffer with only in-range indices; and - executing SQL commands containing no string from external input. In this case, we can implement our approach already in C++ and Java. A more complex case is indexing into an array whose size is known only at run-rime. Statically assuring that this operation is safe without imposing a bound check on each access requires more advanced type systems, such as Java 5 generics, or more generally, higher-rank types as found in OCaml, Scala, or Haskell. Using a mature language with an advanced type system (Haskell), we have extended our approach to statically assure the safety of low-level code such as device drivers. We can ensure 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. We can also enforce protocol and timing requirements, such as that some device register must be read in some order or for some number of times through any execution path in a device driver. Our approach can also be used to prevent arithmetic overflow. This technique is a natural application of our infrastructure for expressing numbers, records, and capabilities in static types. Our technique can make a system more robust against attacks such as SQL injection, buffer overflow, and denial of service. On one hand, our concrete case studies will provide a broad audience of working programmers with a simple way to guard against these attacks and write more secure code. On the other hand, our formal analyses will strengthen the connection between the practice of software reliability and the theory of type soundness, while motivating the use of logic to reason about programs. Oleg Kiselyov and Chung-chieh Shan. 2006. Lightweight static capabilities. In Programming languages meet program verification, ed. Aaron Stump and Hongwei Xi, 2839. Electronic Notes in Theoretical Computer Science, Amsterdam: Elsevier Science. https://okmij.org/ftp/Computation/lightweight-dependent-typing.html#lightweight-static-capabilities Oleg Kiselyov and Chung-chieh Shan. 2007. Lightweight static resources: sexy types for embedded and systems programming. In Trends in Functional Programming. https://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf