Crema: A LangSec-Inspired Programming Language

We discuss the potential for significant reduction in size and complexity of verification tasks for input-handling software when such software follows the LangSec principles, i.e., is designed and compiled for a suitably limited computational model, no stronger than needed for the recognizer automaton of a particular language of inputs. Such a language, Crema is introduced and provided as open-source. We use parts of the qmail parsing code base compared to a restricted parsing environment as a case study, and LLVM and KLEE to estimate the size of its respective verification tasks. We also study the application of the same principles to the verification of reference monitors. Examples of programming with a provably-halting programming language are given as well as how to embed them into your existing programs.