Security monitor inlining and certification for multithreaded Java
2015 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 3, 528-565 p.Article in journal (Refereed) Published
Security monitor inlining is a technique for security policy enforcement whereby monitor functionality is injected into application code in the style of aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). Such inliners are said to be correct. For sequential Java-like languages, inlining is well understood, and several provably correct inliners have been proposed. For multithreaded Java one difficulty is the need to maintain a shared monitor state. We show that this problem introduces fundamental limitations in the type of security policies that can be correctly enforced by inlining. A class of race-free policies is identified that precisely characterizes the inlineable policies by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete inliner for policies inside the class which is secure, conservative and transparent. The inliner is implemented for Java and applied to a number of practical application security policies. Finally, we discuss how certification in the style of proof-carrying code could be supported for inlined programs by using annotations to reduce a potentially complex verification problem for multithreaded Java bytecode to sequential verification of just the inlined code snippets.
Place, publisher, year, edition, pages
2015. Vol. 25, no 3, 528-565 p.
Aspect oriented programming, Codes (symbols), Computer software, Security systems, Application codes, Application security, Fundamental limitations, Java byte codes, Proof-carrying code, Security monitors, Security policy enforcement, Verification problems
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-62964DOI: 10.1017/S0960129512000916ISI: 000348369900003ScopusID: 2-s2.0-84921923104OAI: oai:DiVA.org:kth-62964DiVA: diva2:481441
FunderEU, FP7, Seventh Framework Programme
QC 20150303. Updated from submitted to published.2012-01-202012-01-202015-03-03Bibliographically approved