Provably correct inline monitoring for multithreaded Java-like programs

Issue title: EU-Funded ICT Research on Trust and Security

Guest editors: Jan CamenischGuest-Editor, Javier LopezGuest-Editor, Fabio MassacciGuest-Editor, Massimo CiscatoGuest-Editor and Thomas SkordasGuest-Editor

Article type: Research Article

Authors: Dam, Mads^a | Jacobs, Bart^b | Lundblad, Andreas^c | Piessens, Frank^{d; *}

Affiliations: [a] ACCESS Linnaeus Centre, Royal Institute of Technology (KTH), Sweden. E-mail: mfd@kth.se; Tel.: +46 8 790 6229 | [b] Katholieke Universiteit Leuven, Belgium. E-mail: bart.jacobs@cs.kuleuven.be; Tel.: +32 16 32 7825 | [c] School of Computer Science and Communication, Royal Institute of Technology (KTH), Sweden. E-mail: landreas@kth.se; Tel.: +46 8 790 8408 | [d] Katholieke Universiteit Leuven, Belgium. E-mail: frank.piessens@cs.kuleuven.be; Tel.: +32 16 32 7603

Correspondence: [*] Corresponding author.

Abstract: Inline reference monitoring is a powerful technique to enforce security policies on untrusted programs. The security-by-contract paradigm proposed by the EU FP6 S3MS project uses policies, monitoring, and monitor inlining to secure third-party applications running on mobile devices. The focus of this paper is on multi-threaded Java bytecode. An important consideration is that inlining should interfere with the client program only when mandated by the security policy. In a multi-threaded setting, however, this requirement turns out to be problematic. Generally, inliners use locks to control access to shared resources such as an embedded monitor state. This will interfere with application program non-determinism due to Java's relaxed memory consistency model, and rule out the transparency property, that all policy-adherent behaviour of an application program is preserved under inlining. In its place we propose a notion of strong conservativity, to formalise the property that the inliner can terminate the client program only when the policy is about to be violated. An example inlining algorithm is given and proved to be strongly conservative. Finally, benchmarks are given for four example applications studied in the S3MS project.

Keywords: Security-by-contract, runtime monitoring, monitor inlining

DOI: 10.3233/JCS-2010-0365

Journal: Journal of Computer Security, vol. 18, no. 1, pp. 37-59, 2010