Options
An automatic inference of minimal security types
Publikationstyp
Conference Paper
Date Issued
2015-12
Sprache
English
Author(s)
First published in
Number in series
9478 LNSC
Start Page
395
End Page
415
Citation
Lecture Notes in Computer Science 9478 LNSC: 395-415 (2015)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
Type-based information-flow analyses provide strong end-to-end confidentiality guarantees for programs. Yet, such analyses are not easy to use in practice, as they require all information containers in a program to be annotated with security types, which is a tedious and error-prone task—if done manually. In this article, we propose a new algorithm for inferring such security types automatically. We implement our algorithm as an Eclipse plug-in, which enables software engineers to use it for verifying confidentiality requirements in their programs. We experimentally show our implementation to be effective and efficient. We also analyze theoretical properties of our security-type inference algorithm. In particular, we prove it to be sound, complete, minimal, and of linear time-complexity in the size of the program analyzed.
DDC Class
004: Informatik