Authors:	Keidel, Sven
Title:	Modular Specification and Compositional Soundness of Abstract Interpreters
Online publication date:	15-Oct-2021
Year of first publication:	2021
Language:	english
Abstract:	Static analyses are automated tools that yield information about computer programs without running them. Static analyses are used in modern integrated development environments (IDEs), compilers, and continuous integration servers. For example, IDEs use static analyses to warn developers about common problems such as type errors, dead code, or memory leaks. Compilers use static analyses mainly to optimize the code. For example, a compiler may use a constant analysis to move variable assignments out of loops that do not change. Depending on the use case of a static analysis, the results of the analysis need to be more or less reliable. For example, if a dead code analysis used in an IDE fails to report that a piece of code will never be executed, then the consequences will probably be not that bad. However, if a compiler optimization relies on a faulty analysis, then the optimization may change the semantics of the program. Such a changed program semantics leads to unexpected program behavior and crashes. In these use cases, the unreliable analyses are unacceptable. One way of ensuring that a static analysis is reliable, is to prove that the analysis is sound. Soundness means that a static analysis never fails to report a certain class of bugs or program behavior. For example, a sound static type checker never misses a type error and hence it guarantees that a type correct program executes without crashing. Soundness is especially important for static analyses used in compiler optimizations, for security analyses, and for analyses that verify mission-critical software. Unfortunately, formally proving that a static analysis is sound is difficult. A formal soundness proof shows for all programs, that the analysis result corresponds to the execution of the program. While some complexity of a soundness proof is inherent, a large part is incidental and comes from how the analysis is structured. In particular, many static analyses do not clearly separate different concerns. This coupling often makes a soundness proof infeasible. For example, the analyses in the LLVM compiler have not been proven sound and developers discovered 81 cases of unsoundness since 2010. In this thesis, we propose a methodology for structuring static analyses such that their soundness proof becomes easier. The core principle of this methodology is to make the soundness proof compositional. More specifically, we show how analyses can be implemented modularly with small and reusable components. Each component can be proven sound independently and the composition of components remains sound. This means analysis developers do not need to worry about soundness, as long as they use sound components. We evaluate our methodology by developing several control-flow and data-flow analyses for languages with different programming paradigms. We implemented these analyses by using sound and reusable components of the open-source Haskell library Sturdy (https://github.com/svenkeidel/sturdy), that we developed as part of this thesis. Our experiments show that compositional soundness proofs require less effort, because large parts of the analysis consist of language-independent components that have been proven sound a priori. Furthermore, compositional soundness proofs are less complicated, because components capture only a small piece of functionality, which can be easily proven sound.
DDC:	500 Naturwissenschaften 500 Natural sciences and mathematics
Institution:	Johannes Gutenberg-Universität Mainz
Department:	FB 08 Physik, Mathematik u. Informatik
Place:	Mainz
ROR:	https://ror.org/023b0x485
DOI:	http://doi.org/10.25358/openscience-6384
URN:	urn:nbn:de:hebis:77-openscience-9be985c8-d919-4b03-ab83-d549658968a68
Version:	Original work
Publication type:	Dissertation
License:	CC BY-ND
Information on rights of use:	https://creativecommons.org/licenses/by-nd/4.0/
Extent:	v, 133 Seiten, Illustrationen
Appears in collections:	JGU-Publikationen