{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,7,30]],"date-time":"2023-07-30T19:40:06Z","timestamp":1690746006839},"reference-count":45,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,12,17]],"date-time":"2014-12-17T00:00:00Z","timestamp":1418774400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129512000916","type":"journal-article","created":{"date-parts":[[2014,12,17]],"date-time":"2014-12-17T14:00:03Z","timestamp":1418824803000},"page":"528-565","source":"Crossref","is-referenced-by-count":1,"title":["Security monitor inlining and certification for multithreaded Java"],"prefix":"10.1017","volume":"25","author":[{"given":"MADS","family":"DAM","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BART","family":"JACOBS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ANDREAS","family":"LUNDBLAD","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"FRANK","family":"PIESSENS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,12,17]]},"reference":[{"key":"S0960129512000916_ref42","first-page":"55","volume-title":"Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification, PLPV'11","author":"Sridhar","year":"2011"},{"key":"S0960129512000916_ref39","first-page":"107","article-title":"History effects and verification","author":"Skalka","year":"2004","journal-title":"Asian Programming Languages Symposium"},{"key":"S0960129512000916_ref37","unstructured":"S3MS (2008) Project web page. Available at http:\/\/www.s3ms.org."},{"key":"S0960129512000916_ref36","unstructured":"Reynal S. (2010) Jpicedt website. Available at http:\/\/jpicedt.sourceforge.net\/."},{"key":"S0960129512000916_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"S0960129512000916_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73408-6_21"},{"key":"S0960129512000916_ref32","unstructured":"Lundblad A. (2010) Inlined reference monitors for multithreaded java: Case-studies. Available at http:\/\/www.csc.kth.se\/~landreas\/mt_inlining\/."},{"key":"S0960129512000916_ref41","doi-asserted-by":"crossref","unstructured":"Sridhar M. and Hamlen K. W. (2010b) Model checking in-lined reference monitors. In: Verification, Model Checking, and Abstract Interpretation 312\u2013327.","DOI":"10.1007\/978-3-642-11319-2_23"},{"key":"S0960129512000916_ref29","unstructured":"Ligatti J. A. (2006) Policy Enforcement via Program Monitoring, Ph.D. thesis, Princeton University."},{"key":"S0960129512000916_ref44","unstructured":"Viswanathan M. (2000) Foundations for the Run-Time Analysis of Software Systems, Ph.D. thesis, University of Pennsylvania."},{"key":"S0960129512000916_ref30","volume-title":"Java Virtual Machine Specification","author":"Lindholm","year":"1999"},{"key":"S0960129512000916_ref3","unstructured":"Apache Software Foundation (2002) Servlet api documentation. Available at http:\/\/download.oracle.com\/docs\/cd\/E17802_01\/products\/products\/servlet\/2.5\/docs\/servlet-2_5-mr2\/index.html."},{"key":"S0960129512000916_ref22","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/1134744.1134748","article-title":"Certified in-lined reference monitoring on .NET","author":"Hamlen","year":"2006","journal-title":"Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS'06)"},{"key":"S0960129512000916_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"S0960129512000916_ref27","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025055424017"},{"key":"S0960129512000916_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"S0960129512000916_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00254-3"},{"key":"S0960129512000916_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1111596.1111601"},{"key":"S0960129512000916_ref9","first-page":"200","article-title":"Information flow monitor inlining","author":"Chudnov","year":"2010","journal-title":"Computer Security Foundations"},{"key":"S0960129512000916_ref24","unstructured":"HATS (2010) Evaluation of the core framework, deliverable 5.2 of project fp7-231620 (hats). Available at http:\/\/www.cse.chalmers.se\/research\/hats\/sites\/default\/files\/Deliverable52.pdf."},{"key":"S0960129512000916_ref18","doi-asserted-by":"crossref","unstructured":"Evans D. and Twyman A. (1999) Flexible policy-directed code safety. In: IEEE Symposium on Security and Privacy 32\u201345.","DOI":"10.1109\/SECPRI.1999.766716"},{"key":"S0960129512000916_ref35","unstructured":"OWASP (2010) Owasp top 10 - 2010. Available at http:\/\/owasptop10.googlecode.com\/files\/OWASP%20Top%2010%20-%202010.pdf."},{"key":"S0960129512000916_ref6","first-page":"305","article-title":"Composing security policies with Polymer","author":"Bauer","year":"2005","journal-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)"},{"key":"S0960129512000916_ref17","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/335169.335201","volume-title":"Proceedings of the Workshop on New Security Paradigms (NSPW'99)","author":"Erlingsson","year":"2000"},{"key":"S0960129512000916_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.09.004"},{"key":"S0960129512000916_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325728"},{"key":"S0960129512000916_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.026"},{"key":"S0960129512000916_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"S0960129512000916_ref20","volume-title":"Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley))","author":"Gosling","year":"2005"},{"key":"S0960129512000916_ref14","first-page":"320","article-title":"A flexible measurement tool for software systems","volume":"1","author":"Deutsch","year":"1971","journal-title":"Information Processing 71, Proceeding International Federation for Information Processing Congress"},{"key":"S0960129512000916_ref25","first-page":"193","article-title":"Disambiguating aspect-oriented security policies","author":"Jones","year":"2010","journal-title":"Aspect-Oriented Software Development"},{"key":"S0960129512000916_ref16","article-title":"IRM enforcement of Java stack inspection","author":"Erlingsson","year":"2000","journal-title":"IEEE Symposium on Security and Privacy"},{"key":"S0960129512000916_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375699"},{"key":"S0960129512000916_ref19","doi-asserted-by":"crossref","unstructured":"Franks J. , Hallam-Baker P. , Hostetler J. , Lawrence S. , Leach P. , Luotonen A. and Stewart L. (1999) HTTP authentication: Basic and digest access authentication. Request for Comments 2617 (Draft Standard).","DOI":"10.17487\/rfc2617"},{"key":"S0960129512000916_ref40","doi-asserted-by":"crossref","unstructured":"Sridhar M. and Hamlen K. W. (2010a) Actionscript in-lined reference monitoring in prolog. In: Practical Aspects of Declarative Languages 149\u2013151.","DOI":"10.1007\/978-3-642-11503-5_13"},{"key":"S0960129512000916_ref15","unstructured":"Erlingsson U. (2004) The Inlined Reference Monitor Approach to Security Policy Enforcement. Ph.D. thesis, Department of Computer Science, Cornell University."},{"key":"S0960129512000916_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.02.013"},{"key":"S0960129512000916_ref8","first-page":"546","article-title":"Java-MOP: a monitoring oriented programming environment for Java","author":"Chen","year":"2005","journal-title":"Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"S0960129512000916_ref10","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/978-3-642-03013-0_25","volume-title":"Proceeding of ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genova, Italy, 6\u201310 July, 2009","author":"Dam","year":"2009"},{"key":"S0960129512000916_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.12.002"},{"key":"S0960129512000916_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36532-X_10"},{"key":"S0960129512000916_ref11","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2010-0365"},{"key":"S0960129512000916_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.istr.2008.02.001"},{"key":"S0960129512000916_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0046-8"},{"key":"S0960129512000916_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.01.009"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,30]],"date-time":"2023-07-30T19:04:09Z","timestamp":1690743849000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000916\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,17]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["S0960129512000916"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000916","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,17]]}}}