{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T11:06:24Z","timestamp":1747134384104,"version":"3.38.0"},"reference-count":56,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2015,12,28]],"date-time":"2015-12-28T00:00:00Z","timestamp":1451260800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2016,3,1]]},"abstract":"<jats:p> Recently, much progress has been made on achieving information-flow security via secure multi-execution. Secure multi-execution ([Formula: see text]) is an elegant way to enforce security by executing a given program multiple times, once for each security level, while carefully dispatching inputs and ensuring that an execution at a given level is responsible for producing outputs for information sinks at that level. Secure multi-execution guarantees noninterference, in the sense of no dependencies from secret inputs to public outputs, and transparency, in the sense that if a program is secure then its secure multi-execution does not disable any of its original behavior. <\/jats:p><jats:p> This paper pushes the boundary of what can be achieved with secure multi-execution. First, we lift the assumption from the original secure multi-execution work on the totality of the input environment (that there is always assumed to be input) and on cooperative scheduling. Second, we generalize secure multi-execution to distinguish between security levels of presence and content of messages. Third, we introduce a declassification model for secure multi-execution that allows expressing what information can be released and where it can be released. Fourth, we establish a full transparency result showing how secure multi-execution can preserve the original order of messages in secure programs. We demonstrate that full transparency is a key enabler for discovering attacks with secure multi-execution. <\/jats:p>","DOI":"10.3233\/jcs-150541","type":"journal-article","created":{"date-parts":[[2016,3,4]],"date-time":"2016-03-04T14:39:37Z","timestamp":1457102377000},"page":"39-90","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":13,"title":["Secure multi-execution: Fine-grained, declassification-aware, and transparent"],"prefix":"10.1177","volume":"24","author":[{"given":"Willard","family":"Rafnsson","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]},{"given":"Andrei","family":"Sabelfeld","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]}],"member":"179","published-online":{"date-parts":[[2015,12,28]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"[1]J.\u00a0Agat, Transforming out timing leaks, in: Proc. ACM Symp. on Principles of Programming Languages, 2000, pp.\u00a040\u201353.","DOI":"10.1145\/325694.325702"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"[2]A.\u00a0Askarov and A.\u00a0Sabelfeld, Gradual release: Unifying declassification, encryption and key release policies, in: Proc. IEEE Symp. on Security and Privacy, 2007, pp.\u00a0207\u2013221.","DOI":"10.1109\/SP.2007.22"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"[3]A.\u00a0Askarov and A.\u00a0Sabelfeld, Tight enforcement of information-release policies for dynamic languages, in: Proc. IEEE Computer Security Foundations Symposium, 2009.","DOI":"10.1109\/CSF.2009.22"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"[4]A.\u00a0Askarov, D.\u00a0Zhang and A.C.\u00a0Myers, Predictive black-box mitigation of timing channels, in: CCS, 2010.","DOI":"10.1145\/1866307.1866341"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"[5]T.H.\u00a0Austin and C.\u00a0Flanagan, Efficient purely-dynamic information flow analysis, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2009.","DOI":"10.1145\/1554339.1554353"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"[6]T.H.\u00a0Austin and C.\u00a0Flanagan, Permissive dynamic information flow analysis, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2010.","DOI":"10.1145\/1814217.1814220"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"[7]T.H.\u00a0Austin and C.\u00a0Flanagan, Multiple facets for dynamic information flow, in: Proc. ACM Symp. on Principles of Programming Languages, 2012, pp.\u00a0165\u2013178.","DOI":"10.1145\/2103656.2103677"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"[8]T.H.\u00a0Austin, J.\u00a0Yang, C.\u00a0Flanagan and A.\u00a0Solar-Lezama, Faceted execution of policy-agnostic programs, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), ACM, New York, NY, USA, 2013, pp.\u00a015\u201326.","DOI":"10.1145\/2465106.2465121"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"[9]A.\u00a0Banerjee, D.\u00a0Naumann and S.\u00a0Rosenberg, Expressive declassification policies and modular static enforcement, in: Proc. IEEE Symp. on Security and Privacy, 2008.","DOI":"10.1109\/SP.2008.20"},{"key":"ref010","unstructured":"[10]J.\u00a0Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003."},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"[11]G.\u00a0Barthe, J.M.\u00a0Crespo, D.\u00a0Devriese, F.\u00a0Piessens and E.\u00a0Rivas, Secure multi-execution through static program transformation, in: Formal Techniques for Distributed Systems (FMOODS\/FORTE 2012), LNCS, Vol.\u00a07273, 2012, pp.\u00a0186\u2013202.","DOI":"10.1007\/978-3-642-30793-5_12"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"[12]N.\u00a0Bielova, D.\u00a0Devriese, F.\u00a0Massacci and F.\u00a0Piessens, Reactive non-interference for a browser model, in: Proc. 5th International Conference on Network and System Security (NSS), 2011.","DOI":"10.1109\/ICNSS.2011.6059965"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"[13]N.\u00a0Bielova, D.\u00a0Devriese, F.\u00a0Massacci and F.\u00a0Piessens, Reactive non-interference for the browser: Extended version, Technical Report CW602, CS Dept., K.U. Leuven, 2011.","DOI":"10.1109\/ICNSS.2011.6059965"},{"key":"ref014","unstructured":"[14]A.\u00a0Bohannon and B.C.\u00a0Pierce, Featherweight Firefox: Formalizing the core of a web browser, in: Proc. USENIX Conference on Web Application Development, 2010."},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"[15]A.\u00a0Bohannon, B.C.\u00a0Pierce, V.\u00a0Sj\u00f6berg, S.\u00a0Weirich and S.\u00a0Zdancewic, Reactive noninterference, in: ACM Conference on Computer and Communications Security, 2009, pp.\u00a079\u201390.","DOI":"10.1145\/1653662.1653673"},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"[16]R.\u00a0Capizzi, A.\u00a0Longo, V.N.\u00a0Venkatakrishnan and A.\u00a0Prasad Sistla, Preventing information leaks through shadow executions, in: Annual Computer Security Applications Conference (ACSAC), 2008, pp.\u00a0322\u2013331.","DOI":"10.1109\/ACSAC.2008.50"},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"[17]D.\u00a0Clark and S.\u00a0Hunt, Noninterference for deterministic interactive programs, in: Workshop on Formal Aspects in Security and Trust (FAST\u201908), 2008.","DOI":"10.1007\/978-3-642-01465-9_4"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"[18]W.\u00a0De Groef, D.\u00a0Devriese, N.\u00a0Nikiforakis and F.\u00a0Piessens, FlowFox: A web browser with flexible and precise information flow control, in: ACM Conference on Computer and Communications Security, 2012.","DOI":"10.1145\/2382196.2382275"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"[20]D.\u00a0Devriese and F.\u00a0Piessens, Non-interference through secure multi-execution, in: Proc. IEEE Symp. on Security and Privacy, 2010.","DOI":"10.1109\/SP.2010.15"},{"key":"ref021","unstructured":"[21]C.\u00a0Dima, C.\u00a0Enea and R.\u00a0Gramatovici, Nondeterministic nointerference and deducible information flow, Technical Report 2006-01, LACL, University of Paris 12, 2006."},{"key":"ref022","doi-asserted-by":"crossref","unstructured":"[22]J.A.\u00a0Goguen and J.\u00a0Meseguer, Security policies and security models, in: Proc. IEEE Symp. on Security and Privacy, 1982, pp.\u00a011\u201320.","DOI":"10.1109\/SP.1982.10014"},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"[23]D.\u00a0Hedin and A.\u00a0Sabelfeld, Information-flow security for a core of Javascript, in: Proc. IEEE Computer Security Foundations Symposium, 2012, pp.\u00a03\u201318.","DOI":"10.1109\/CSF.2012.19"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"[24]M.\u00a0Jaskelioff and A.\u00a0Russo, Secure multi-execution in Haskell, in: Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS, Vol.\u00a07162, Springer-Verlag, 2011, pp.\u00a0170\u2013178.","DOI":"10.1007\/978-3-642-29709-0_16"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"[25]V.\u00a0Kashyap, B.\u00a0Wiedermann and B.\u00a0Hardekopf, Timing- and termination-sensitive secure information flow: Exploring a new approach, in: Proc. IEEE Symp. on Security and Privacy, 2011.","DOI":"10.1109\/SP.2011.19"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"[26]G.\u00a0Le Guernic, Confidentiality enforcement using dynamic information flow analyses, PhD thesis, Kansas State University, 2007.","DOI":"10.1007\/978-3-540-76929-3_4"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"[27]G.\u00a0Le Guernic, Automaton-based confidentiality monitoring of concurrent programs, in: Proc. IEEE Computer Security Foundations Symposium, 2007, pp.\u00a0218\u2013232.","DOI":"10.1109\/CSF.2007.10"},{"key":"ref028","unstructured":"[28]G.\u00a0Le Guernic, A.\u00a0Banerjee, T.\u00a0Jensen and D.\u00a0Schmidt, Automata-based confidentiality monitoring, in: Proc. Asian Computing Science Conference (ASIAN\u201906), LNCS, Vol.\u00a04435, Springer-Verlag, 2006."},{"key":"ref029","doi-asserted-by":"crossref","unstructured":"[29]P.\u00a0Li and S.\u00a0Zdancewic, Downgrading policies and relaxed noninterference, in: Proc. ACM Symp. on Principles of Programming Languages, 2005, pp.\u00a0158\u2013170.","DOI":"10.1145\/1047659.1040319"},{"key":"ref030","doi-asserted-by":"crossref","unstructured":"[30]H.\u00a0Mantel, Information flow control and applications \u2013 Bridging a gap, in: Proc. Formal Methods Europe, LNCS, Vol.\u00a02021, Springer-Verlag, 2001, pp.\u00a0153\u2013172.","DOI":"10.1007\/3-540-45251-6_9"},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"[31]H.\u00a0Mantel and D.\u00a0Sands, Controlled downgrading based on intransitive (non)interference, in: Proc. Asian Symp. on Programming Languages and Systems, LNCS, Vol.\u00a03302, Springer-Verlag, 2004, pp.\u00a0129\u2013145.","DOI":"10.1007\/978-3-540-30477-7_9"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"[32]A.C.\u00a0Myers, A.\u00a0Sabelfeld and S.\u00a0Zdancewic, Enforcing robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2004, pp.\u00a0172\u2013186.","DOI":"10.1109\/CSFW.2004.1310740"},{"key":"ref033","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2006-14203"},{"key":"ref034","unstructured":"[34]A.C.\u00a0Myers, L.\u00a0Zheng, S.\u00a0Zdancewic, S.\u00a0Chong and N.\u00a0Nystrom, Jif: Java information flow. Software release, 2001, available at: http:\/\/www.cs.cornell.edu\/jif."},{"key":"ref035","doi-asserted-by":"crossref","unstructured":"[35]N.\u00a0Nikiforakis, L.\u00a0Invernizzi, A.\u00a0Kapravelos, S.\u00a0Van Acker, W.\u00a0Joosen, C.\u00a0Kruegel, F.\u00a0Piessens and G.\u00a0Vigna, You are what you include: Large-scale evaluation of remote Javascript inclusions, in: ACM Conference on Computer and Communications Security, 2012, pp.\u00a0736\u2013747.","DOI":"10.1145\/2382196.2382274"},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"[36]K.\u00a0O\u2019Neill, M.\u00a0Clarkson and S.\u00a0Chong, Information-flow security for interactive programs, in: Proc. IEEE Computer Security Foundations Workshop, 2006, pp.\u00a0190\u2013201.","DOI":"10.1109\/CSFW.2006.16"},{"key":"ref037","doi-asserted-by":"crossref","unstructured":"[37]W.\u00a0Rafnsson, D.\u00a0Hedin and A.\u00a0Sabelfeld, Securing interactive programs, in: Proc. IEEE Computer Security Foundations Symposium, 2012.","DOI":"10.1109\/CSF.2012.15"},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"[38]W.\u00a0Rafnsson and A.\u00a0Sabelfeld, Limiting information leakage in event-based communication, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2011.","DOI":"10.1145\/2166956.2166960"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"[39]W.\u00a0Rafnsson and A.\u00a0Sabelfeld, Secure multi-execution: Fine-grained, declassification-aware, and transparent, in: Proc. IEEE Computer Security Foundations Symposium, 2013, pp.\u00a03\u201318.","DOI":"10.1109\/CSF.2013.10"},{"key":"ref040","doi-asserted-by":"crossref","unstructured":"[40]A.\u00a0Russo, J.\u00a0Hughes, D.\u00a0Naumann and A.\u00a0Sabelfeld, Closing internal timing channels by transformation, in: Proc. Asian Computing Science Conference (ASIAN\u201906), LNCS, Vol.\u00a04435, Springer-Verlag, 2007.","DOI":"10.1007\/978-3-540-77505-8_10"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"[41]A.\u00a0Russo and A.\u00a0Sabelfeld, Securing timeout instructions in web applications, in: Proc. IEEE Computer Security Foundations Symposium, 2009.","DOI":"10.1109\/CSF.2009.16"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"[42]A.\u00a0Russo and A.\u00a0Sabelfeld, Dynamic vs. static flow-sensitive security analysis, in: Proc. IEEE Computer Security Foundations Symposium, 2010.","DOI":"10.1109\/CSF.2010.20"},{"key":"ref043","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref044","doi-asserted-by":"crossref","unstructured":"[44]A.\u00a0Sabelfeld and A.C.\u00a0Myers, A model for delimited information release, in: Proc. International Symp. on Software Security (ISSS\u201903), LNCS, Vol.\u00a03233, Springer-Verlag, 2004, pp.\u00a0174\u2013191.","DOI":"10.1007\/978-3-540-37621-7_9"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"[45]A.\u00a0Sabelfeld and A.\u00a0Russo, From dynamic to static and back: Riding the roller coaster of information-flow control research, in: Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS, Vol.\u00a05947, Springer-Verlag, 2009.","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0352"},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"[47]P.\u00a0Shroff, S.\u00a0Smith and M.\u00a0Thober, Dynamic dependency monitoring to secure information flow, in: Proc. IEEE Computer Security Foundations Symposium, 2007, pp.\u00a0203\u2013217.","DOI":"10.1109\/CSF.2007.20"},{"key":"ref048","unstructured":"[48]V.\u00a0Simonet, The Flow Caml system. Software release, 2003, available at: http:\/\/cristal.inria.fr\/~simonet\/soft\/flowcaml."},{"key":"ref049","unstructured":"[49]N.\u00a0Singer and C.\u00a0Duhigg, Tracking voters\u2019 clicks online to try to sway them, 2012, available at: http:\/\/www.nytimes.com\/2012\/10\/28\/us\/politics\/tracking-clicks-online-to-try-to-sway-voters.html."},{"key":"ref050","unstructured":"[50]Syrian Electronic Army uses Taboola ad to hack Reuters (again), available at: https:\/\/nakedsecurity.sophos.com\/2014\/06\/23\/syrian-electronic-army-uses-taboola-ad-to-hack-reuters-again\/."},{"key":"ref051","doi-asserted-by":"crossref","unstructured":"[51]H.\u00a0Unno, N.\u00a0Kobayashi and A.\u00a0Yonezawa, Combining type-based analysis and model checking for finding counterexamples against non-interference, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2006, pp.\u00a017\u201326.","DOI":"10.1145\/1134744.1134750"},{"key":"ref052","doi-asserted-by":"crossref","unstructured":"[52]M.\u00a0Vanhoef, W.\u00a0De Groef, D.\u00a0Devriese, F.\u00a0Piessens and T.\u00a0Rezk, Stateful declassification policies for event-driven programs, in: CSF, 2014.","DOI":"10.1109\/CSF.2014.28"},{"key":"ref053","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"ref054","doi-asserted-by":"crossref","unstructured":"[54]J.\u00a0Yang, K.\u00a0Yessenov and A.\u00a0Solar-Lezama, A language for automatically enforcing privacy policies, in: POPL, 2012, pp.\u00a085\u201396.","DOI":"10.1145\/2103656.2103669"},{"key":"ref055","doi-asserted-by":"crossref","unstructured":"[55]D.\u00a0Zanarini, M.\u00a0Jaskelioff and A.\u00a0Russo, Precise enforcement of confidentiality for reactive system, in: Proc. IEEE Computer Security Foundations Symposium, 2013.","DOI":"10.1109\/CSF.2013.9"},{"key":"ref056","doi-asserted-by":"crossref","unstructured":"[56]S.\u00a0Zdancewic and A.C.\u00a0Myers, Robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2001, pp.\u00a015\u201323.","DOI":"10.1109\/CSFW.2001.930133"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-150541","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-150541","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-150541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T05:31:47Z","timestamp":1741671107000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-150541"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,28]]},"references-count":56,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3,1]]}},"alternative-id":["10.3233\/JCS-150541"],"URL":"https:\/\/doi.org\/10.3233\/jcs-150541","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"type":"print","value":"0926-227X"},{"type":"electronic","value":"1875-8924"}],"subject":[],"published":{"date-parts":[[2015,12,28]]}}}