@MASTERSTHESIS\{IMM2015-06896,
    author       = "T. Maciazek",
    title        = "Content-Based Information Flow Verification for C",
    year         = "2015",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Richard Petersens Plads, Building 324, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: Hanne Riis Nielson, hrni@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    abstract     = "Integration of hardware and software in avionics industry started in 1990s and was followed by increasing interconnectivity with external networks. Since then, the companies producing planes, designed for military and public transport alike, struggled with not only the safety, but also security problems. The certification processes that they were already using for safety had to be extended with security concerns, as these could also impact safety. Concepts such as Integrated Modular Avionics (IMA) and later Multiple Independent Levels of Security (MILS) emerged. They leveraged modularity of previously separate components and proposed solutions for controlling information flow between them. Those solutions involved enforcement of separation and restriction of communication, using separation kernels capable of securely partitioning resources, and secure gateways that could examine the content of the exchanged messages and filter them.

Although the proposed solutions considerably reduced the costs of certification for those safety-critical systems, the code ensuring separation and filtering was still required to display correctness assurance. This has lead to development of static analysis techniques allowing automatic verification of such code, where the Decentralized Label Model (DLM) seemed to be the most promising tool. Unfortunately, {DLM} proved to be insufficient, as it cannot be used to provide assurance for a code where the labels (the {DLM} version of policies) are content-dependent. An obvious solution was to augment {DLM} with such content-dependent policies, however, this introduced another problem – the necessity to reason about the possible states which the program may be in.

This work builds on the previous works in this topic and introduces a version of {DLM} with content-dependent policies for a subset of the C programming language. A formal type system, which uses Hoare logic to reason about the state of the program, is built and thoroughly explained on examples. Another product of this work is a C\# implementation of a verification tool called C2if, which is based on that type system. The implementation uses Z3, an {SMT} solver, as the core for the state- and constraint-based reasoning, and {ATLR,} a parser generator, as the tool for generating an abstract syntax tree (AST) from the input code."
}