2012 | OriginalPaper | Buchkapitel
Challenges in Defining a Programming Language for Provably Correct Dynamic Analyses
verfasst von : Eric Bodden, Andreas Follner, Siegfried Rasthofer
Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.