DocumentCode :
3532095
Title :
Abstract Interpretation in Code Security
Author :
Giacobazzi, Roberto
Author_Institution :
Univ. of Verona, Verona
fYear :
2008
fDate :
10-14 Nov. 2008
Firstpage :
3
Lastpage :
3
Abstract :
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.
Keywords :
programming language semantics; security of data; abstract noninterference; code security; language based security; semantic based approach; Computer languages; Concrete; Information analysis; Information security; Lattices; Runtime; Software engineering; Transformers;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering and Formal Methods, 2008. SEFM '08. Sixth IEEE International Conference on
Conference_Location :
Cape Town
Print_ISBN :
978-0-7695-3437-4
Type :
conf
DOI :
10.1109/SEFM.2008.49
Filename :
4685788
Link To Document :
بازگشت