Abstract Interpretation in Code Security

In this tutorial we will consider abstract non-interference as a formal model for reasoning about language based security. Abstract non-interference generalises standard non-interference by modelling the information leaked as abstract properties of concrete computations. In this case abstractions model both the observational capabilities of attackers and the amount of information that may flow between program components, e.g., from private to public variables, dynamically at run-time. We prove that abstract non-interference generalizes known models of attackers in language-based security and provides at the same time a formal setting for comparing many of the known approaches for weakening non-interference. We introduce a proof system for checking abstract non-interference and systematic methods, i.e., abstraction transformers, for deriving the most concrete harmless attacker for which a program is secure together with the corresponding maximal amount of information released. This provides the possibility of associating programs with canonical attackers and compare them according to their relative degree of security in the lattice of abstract interpretations. Due to its semantic-based approach and the generality of abstract interpretation and non-interference notions, abstract non-interference can be fairly considered as a unifying theory for understanding and reasoning about information-flow in programming languages, including security, program slicing and dependence analysis as special cases.