Challenges in defining a programming language for provably correct dynamic analyses
Eric | October 12, 2012
Our work Challenges in defining a programming language for provably correct dynamic analyses, to be presented at ISOLA next week, describes the challenges involved in designing a new programming language that we plan to develop. This new language is at the core of my new project RUNSECURE. The language is meant to target security experts, who can use it to implement enforcement monitors that when applied to a potentially insecure program will automatically secure the program against certain classes of attacks.
From the paper abstract:
Modern software systems are not only famous for being ubiquitous and large scale but also infamous for being inherently insecure. We argue that a large part of this problem is due to the fact that current programming languages do not provide adequate built-in support for addressing security concerns.
In this work we outline the challenges involved in developing CODANA, a novel programming language for defining provably correct dynamic analyses. CODANA analyses form security monitors; they allow programmers to proactively protect their programs from security threats such as insecure information flows, buffer overflows and access-control violations. We plan to design CODANA in such a way that program analyses will be simple to write, read and prove correct, easy to maintain and reuse, efficient to compile, easy to parallelize, and maximally amenable to static optimizations. This is difficult as, nevertheless, CODANA must comprise sufficiently expressive language constructs to cover a large class of security-relevant dynamic analyses.
For deployed programs, we envision CODANA-based analyses to be the last line of defense against malicious attacks. It is hence paramount to provide correctness guarantees on CODANA-based analyses as well as the related program instrumentation and static optimizations.
A further challenge is effective but provably correct sharing: dynamic analyses can benefit from sharing information among another. We plan to encapsulate such shared information within CODANA program fragments.
This is joint work with my new PhD students Andreas Follner and Siegfried Rasthofer.
