Analysing Information Flow Properties in Assembly Code by Abstract Interpretation

This paper presents an approach to analyze stack-based assembly code with respect to leakages of private information. We consider systems implementing a multilevel security policy, where the security levels form a lattice. The approach is based on abstract interpretation of the operational semantics. We consider a representative subset of instructions of conventional stack-based assembly languages. We define a collecting small-step semantics of the language, enhanced to convey the level of the information flow during execution: this is accomplished by annotating each value with the level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level. We give sufficient conditions the abstract semantics must satisfy to ensure secure information flow. The use of abstract interpretation allows, on one side, being semantics based, to accept as secure a wide class of programs, and on the other side, being rule based, to be automated fully. In fact we show how it may be combined with a model checking technique, where the conditions for security are described by temporal logic formulae that can be automatically checked on the abstract representation of the program.