Correctness-by-Construction for Correct and Secure Software Systems

Ensuring the safety and security of software systems is more important today than ever before, as critical domains (such as automotive, aviation, or healthcare systems) become increasingly software-intensive. Typically, such critical software is exhaustively tested, but testing alone cannot guarantee correctness. Therefore, formal approaches are required to ensure safety and security of the developed software. For functional correctness, post-hoc verification is the state-of-the-art. By post-hoc verification, we mean that a program is implemented, specified with a pre-/postcondition contract, and then verified. However, this approach has the downside that it does not provide guidelines for developers how to write correct code. If a program developed without guidelines cannot be verified, it is often difficult to find the root causes. It may be a faulty implementation or an unsuitable specification of the program. As a result, it is costly to debug the program and to verify it again. In terms of security, it is important to ensure confidentiality and integrity of processed data. Here, static and dynamic taint analysis approaches are prevalent, where data is labeled with a security level to analyze whether there is a prohibited flow from a secure source to a public sink as defined by a security policy. ... mehrThis post-hoc analysis has the same disadvantage as post-hoc verification, an incorrect program must be debugged and then reanalyzed to ensure that the vulnerability is fixed. The general drawback of post-hoc analysis and verification techniques is that they reveal problems in the code, but do not assist in correcting them. Correctness-by-Construction (CbC) is an alternative program development approach in which a program is directly constructed to be correct. Starting with a specified, but abstract program, a set of refinement rules is applied to refine the program into a concrete implementation. Each applied refinement rule guarantees that the program under development satisfies the initial specification. Thus, the resulting program is correct by construction. It is argued that with the CbC approach, defects are discovered at an early stage of development and can be resolved more easily through a structured program development approach. Despite these benefits, CbC has not yet become an established development approach for safety- and security-critical software. We identified three main reasons/challenges: (1) lack of tool support, (2) rigid program development due to the fine-grained refinement rules that allow only one program statement to be added at a time, (3) and no CbC approach to ensure non-functional properties, such as information flow security. In this thesis, we provide remedy to the aforementioned challenges by establishing and supporting a correct-by-construction program development approach for functionally correct and secure programs. In particular, we make the following four contributions in this thesis. As a first contribution, we implement \corc, tool support for CbC. We determine the requirements to enable CbC for correct program development and develop tool support accordingly. \corc ensures that the correctness of the program under development is ensured in each construction step. In the second contribution, we conduct user studies to determine the comprehensibility and usability of \corc. In the user studies, we are able to analyze how developers proceed to solve programming tasks, what mistakes they make, and how they like using the tool. We compare these results to state-of-the-art program development with post-hoc verification. As third contribution, we address the rigid program development approach of classic CbC by considering new approaches that allow for more flexible program construction. We introduce new refinement rules that condense the application of other refinement rules. We also propose a new trait-based CbC development approach that is based on program composition instead of refinement rules. Since CbC only considers functional correctness up to our work, we extend CbC to also ensure secure information flow in our fourth contribution. We develop refinement rules that ensure program conformance with information flow security policies. At each refinement step, the information flow is analyzed to allow only secure program statements. The refinement rules are integrated into \corc to provide tool support for the constructive development of secure software, and we demonstrate the feasibility of \corc by correctly constructing several case studies. In summary, our work enables the development of functionally correct and secure programs using correctness-by-construction. This foundation can be used to determine whether CbC is a viable alternative to post-hoc verification or post-hoc analysis.