Ph.D. thesis: From Formal Semantics to Verified Slicing - A Modular Framework with Applications in Language Based Security

This thesis presents a modular framework for slicing in the proof assistant Isabelle/HOL which is based on abstract control flow graphs. Building on such abstract structures renders the correctness results in the framework language-independent. To prove that they hold for a specific language, it remains to instantiate the framework with this language, i.e., show that the control flow graph of a program fulfills the properties of the framework.

This requires a formal semantics of this language in Isabelle/HOL. The first part of this thesis shows that formal semantics even for sophisticated high-level languages are realizable. I formalize the formal semantics of a C++ kernel language focusing on C++'s inheritance mechanisms. Inheritance in C++ is complex as it allows (i) multiple inheritance and (ii) two different kinds of inheritance relations. An important result of this work is the first proof that inheritance a la C++ does not compromise type safety.

In the second part, this thesis provides correctness proofs for dynamic as well as static intra- and interprocedural slicing. Prior works only examine intraprocedural slicing and are restricted to simple imperative languages. In contrast, this thesis also proves the context-sensitive interprocedural slicing algorithm by Horwitz, Reps, and Binkley correct; this is the first formal correctness result on this standard algorithm.

By instantiating the framework with two different languages, I show that the abstraction chosen in the framework are indeed sensible. Finally, via the correctness of slicing, this thesis proves that slicing can guarantee classical noninterference, an important result for the Quis custodiet project. All proofs in this thesis are carried out in the proof assistant Isabelle/HOL.