research-article

Security of multithreaded programs by compilation

Authors:

Alejandro Russo,

Andrei SabelfeldAuthors Info & Claims

ACM Transactions on Information and System Security (TISSEC), Volume 13, Issue 3

Article No.: 21, Pages 1 - 32

https://doi.org/10.1145/1805974.1805977

Published: 30 July 2010 Publication History

Abstract

End-to-End security of mobile code requires that the code neither intentionally nor accidentally propagates sensitive information to an adversary. Although mobile code is commonly multithreaded low-level code, there lack enforcement mechanisms that ensure information security for such programs. The modularity is three-fold: we give modular extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow us enforcing security for multithreaded programs. Thanks to the modularity, there are no more restrictions on multithreaded source programs than on sequential ones, and yet we guarantee that their compilations are provably secure for a wide class of schedulers.

References

[1]

Abadi, M. 1998. Protection in programming-language translations. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag, Berlin, 868--883.

Digital Library

[2]

Agat, J. 2000. Transforming out timing leaks. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 40--53.

Digital Library

[3]

Almeida Matos, A. 2006. Typing secure information flow: Declassification and mobility. Ph.D. thesis, Ecole Nationale Supérieure des Mines de Paris.

[4]

Banerjee, A. and Naumann, D. A. 2005. Stack-based access control and secure information flow. J. Funct. Program. 15, 2, 131--177.

Digital Library

[5]

Barnes, J. and Barnes, J. 2003. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman, Boston.

Digital Library

[6]

Barthe, G., Pichardie, D., and Rezk, T. 2007. A certified lightweight non-interference java bytecode verifier. In Proceedings of the European Symposium on Programming. Springer, Berlin.

Digital Library

[7]

Barthe, G. and Rezk, T. 2005. Non-interference for a JVM-like language. In Proceedings of the International Workshop on Types of Languages Design and Implementation. ACM, New York, 103--112.

Digital Library

[8]

Barthe, G., Rezk, T., and Basu, A. 2007. Security types preserving compilation. J. Comput. Lang. Syst. Struct.

Digital Library

[9]

Barthe, G., Rezk, T., and Naumann, D. 2006. Deriving an information flow checker and certifying compiler for java. In Proceedings of the Symposium on Security and Privacy. IEEE, Los Alamitos, CA, 230--242.

Digital Library

[10]

Barthe, G., Rezk, T., Russo, A., and Sabelfeld, A. 2007. Security of multithreaded programs by compilation. In Proceedings of the European Symposium on Research in Computer Security. Springer-Verlag, Berlin, 2--18.

Digital Library

[11]

Barthe, G., Rezk, T., Russo, A., and Sabelfeld, A. 2009. Security of multithreaded programs by compilation. Full version. Tech. rep. http://www.cse.chalmers.se/~russo/tissecfull.pdf.

[12]

Boudol, G. and Castellani, I. 2002. Noninterference for concurrent programs and thread systems. Theor. Comput. Sci. 281, 1, 109--130.

Digital Library

[13]

Chapman, R. and Hilton, A. 2004. Enforcing security and safety models with an information flow analysis tool. ACM SIGAda Ada Lett. 24, 4, 39--46.

Digital Library

[14]

Denning, D. E. and Denning, P. J. 1977. Certification of programs for secure information flow. Comm. ACM 20, 7, 504--513.

Digital Library

[15]

Focardi, R. and Gorrieri, R. 2001. Classification of security properties (Part I: Information flow). In Foundations of Security Analysis and Design, R. Focardi and R. Gorrieri, Eds. Springer-Verlag, Berlin, 331--396.

Digital Library

[16]

Genaim, S. and Spoto, F. 2005. Information flow analysis for Javab. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, Berlin, 346--362.

Digital Library

[17]

Goguen, J. A. and Meseguer, J. 1982. Security policies and security models. In Proceedings of the Symposium on Security and Privacy. IEEE, Los Alamitos, CA, 11--20.

[18]

Hedin, D. and Sands, D. 2006. Noninterference in the presence of non-opaque pointers. In Proceedings of the 19th Computer Security Foundations Workshop. IEEE, Los Alamitos, CA, 255--269.

Digital Library

[19]

Honda, K., Vasconcelos, V., and Yoshida, N. 2000. Secure information flow as typed process behaviour. In Proceedings of the European Symposium on Programming. Springer-Verlag, Berlin, 180--199.

Digital Library

[20]

Honda, K. and Yoshida, N. 2002. A uniform type structure for secure information flow. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 81--92.

Digital Library

[21]

Huisman, M., Worah, P., and Sunesen, K. 2006. A temporal logic characterisation of observational determinism. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA.

Digital Library

[22]

Knudsen, J. 2002. Networking, user experience, and threads. Sun Technical Articles and Tips http://developers.sun.com/techtopics/mobility/midp/articles/threading/.

[23]

Köpf, B. and Mantel, H. 2006. Eliminating implicit information leaks by transformational typing and unification. In Proceedings of the 3rd International Workshop on Formal Aspects in Security and Trust. Springer-Verlag, Berlin, 47--62.

Digital Library

[24]

Mahmoud, Q. H. 2004. Preventing screen lockups of blocking operations. Sun Technical Articles and Tips. http://developers.sun.com/techtopics/mobility/midp/ttips/screenlock/.

[25]

Medel, R., Compagnoni, A., and Bonelli, E. 2005. A typed assembly language for noninterference. In Proceedings of the Italian Conference on Theoretical Computer Science. Springer-Verlag, Berlin, 360--374.

Digital Library

[26]

Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21, 3, 528--569.

Digital Library

[27]

Myers, A. C. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 228--241.

Digital Library

[28]

Myers, A. C., Zheng, L., Zdancewic, S., Chong, S., and Nystrom, N. 2001. JIF: Java information flow. Software release. http://www.cs.cornell.edu/jif.

[29]

Necula, G. C. 1997. Proof-carrying code. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 106--119.

Digital Library

[30]

Pottier, F. 2002. A simple view of type-secure information flow in the pi-calculus. In Proceedings of the IEEE Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 320--330.

Digital Library

[31]

Pottier, F. and Simonet, V. 2003. Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25, 1, 117--158.

Digital Library

[32]

Rezk, T. 2006. Verification of confidentiality policies for mobile code. Ph.D. thesis, Université de Nice Sophia-Antipolis.

[33]

Russo, A., Hughes, J., Naumann, D., and Sabelfeld, A. 2007. Closing internal timing channels by transformation. In Proceedings of the Asian Computing Science Conference. Springer-Verlag, Berlin.

Digital Library

[34]

Russo, A. and Sabelfeld, A. 2006a. Securing interaction between threads and the scheduler. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 177--189.

Digital Library

[35]

Russo, A. and Sabelfeld, A. 2006b. Security for multithreaded programs under cooperative scheduling. In Proceedings of the Andrei Ershov International Conference on Perspectives of System Informatics. Springer-Verlag, Berlin.

Digital Library

[36]

Ryan, P. 2001. Mathematical models of computer security—tutorial lectures. In Foundations of Security Analysis and Design, R. Focardi and R. Gorrieri, Eds. Springer-Verlag, Berlin, 1--62.

Digital Library

[37]

Sabelfeld, A. 2001. The impact of synchronisation on secure information flow in concurrent programs. In Proceedings of the Andrei Ershov International Conference on Perspectives of System Informatics. Springer-Verlag, Berlin, 225--239.

Digital Library

[38]

Sabelfeld, A. and Mantel, H. 2002. Static confidentiality enforcement for distributed programs. In Proceedings of the Symposium on Static Analysis. Springer-Verlag, Berlin, 376--394.

[39]

Sabelfeld, A. and Myers, A. C. 2003. Language-based information-flow security. IEEE J. Sel. Areas Comm. 21, 1, 5--19.

Digital Library

[40]

Sabelfeld, A. and Sands, D. 2000. Probabilistic noninterference for multi-threaded programs. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 200--214.

Digital Library

[41]

Simonet, V. 2003. The Flow Caml system. Software release. http://cristal.inria.fr/_simonet/soft/flowcaml/.

[42]

Smith, G. 2001. A new type system for secure information flow. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 115--125.

Digital Library

[43]

Smith, G. 2003. Probabilistic noninterference through weak probabilistic bisimulation. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 3--13.

[44]

Smith, G. and Volpano, D. 1998. Secure information flow in a multithreaded imperative language. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 355--364.

Digital Library

[45]

Terauchi, T. 2008. A type system for observational determinism. In Proceedings of the 21st Computer Security Foundations Symposium. IEEE, Los Alamitos, CA.

Digital Library

[46]

Tsai, T. C., Russo, A., and Hughes, J. 2007. A library for secure multithreaded information flow in Haskell. In Proceedings of the 20th Computer Security Foundations Symposium. IEEE, Los Alamitos, CA.

Digital Library

[47]

van der Meyden, R. and Zhang, C. 2008. Information flow in systems with schedulers. In Proceedings of the Computer Security Foundation Symposium. IEEE, Los Alamitos, CA.

Digital Library

[48]

Volpano, D. and Smith, G. 1999. Probabilistic noninterference in a concurrent language. J. Comput. Secur. 7, 2--3, 231--253.

Digital Library

[49]

Volpano, D., Smith, G., and Irvine, C. 1996. A sound type system for secure flow analysis. J. Comput. Secur. 4, 3, 167--187.

Digital Library

[50]

Zanardini, D. 2006. Abstract noninterference in a fragment of java bytecode. In Proceedings of the Symposium on Applied Computing. ACM, New York, 1822--1826.

Digital Library

[51]

Zdancewic, S. and Myers, A. C. 2003. Observational determinism for concurrent program security. In Proceedings of the Computer Security Foundations Symposium. IEEE, Los Alamitos, CA, 29--43.

Cited By

Ghosal SShyamasundar RJuristo N(2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-NIER52604.2021.00015
SISON RMURRAY T(2021)Verified secure compilation for mixed-sensitivity concurrent programsJournal of Functional Programming10.1017/S095679682100016231Online publication date: 28-Jul-2021
https://doi.org/10.1017/S0956796821000162
Ghosal SShyamasundar R(2020)A Generalized Notion of Non-interference for Flow Security of Sequential and Concurrent Programs2020 27th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC51365.2020.00013(51-60)Online publication date: Dec-2020
https://doi.org/10.1109/APSEC51365.2020.00013
Show More Cited By

Index Terms

Security of multithreaded programs by compilation

Recommendations

Security of multithreaded programs by compilation
ESORICS'07: Proceedings of the 12th European conference on Research in Computer Security

Information security is a pressing challenge for mobile code technologies. In order to claim end-to-end security of mobile code, it is necessary to establish that the code neither intentionally nor accidentally propagates sensitive information to an ...
Debugging Multithreaded Programs that Incorporate User-Level Locking
A survey of race bug detection techniques for multithreaded programmes

As multithreaded programmes become popular to fully utilize multicore CPUs, many race bug detection techniques have been developed to find concurrency errors in multithreaded programmes effectively. Because these techniques have different views on ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Information and System Security

ACM Transactions on Information and System Security Volume 13, Issue 3

July 2010

253 pages

ISSN:1094-9224

EISSN:1557-7406

DOI:10.1145/1805974

Issue’s Table of Contents

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 July 2010

Accepted: 01 July 2009

Received: 01 June 2008

Published in TISSEC Volume 13, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
318
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ghosal SShyamasundar RJuristo N(2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-NIER52604.2021.00015
SISON RMURRAY T(2021)Verified secure compilation for mixed-sensitivity concurrent programsJournal of Functional Programming10.1017/S095679682100016231Online publication date: 28-Jul-2021
https://doi.org/10.1017/S0956796821000162
Ghosal SShyamasundar R(2020)A Generalized Notion of Non-interference for Flow Security of Sequential and Concurrent Programs2020 27th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC51365.2020.00013(51-60)Online publication date: Dec-2020
https://doi.org/10.1109/APSEC51365.2020.00013
Darais DSweet ILiu CHicks M(2019)A language for probabilistically oblivious computationProceedings of the ACM on Programming Languages10.1145/33711184:POPL(1-31)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371118
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Karbyshev ASvendsen KAskarov ABirkedal L(2018)Compositional Non-interference for Concurrent Programs via Separation and FramingPrinciples of Security and Trust10.1007/978-3-319-89722-6_3(53-78)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89722-6_3
Patrignani MGarg D(2017)Secure Compilation and Hyperproperty Preservation2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.13(392-404)Online publication date: Aug-2017
https://doi.org/10.1109/CSF.2017.13
Vassena MRusso AMurray TStefan D(2016)On Formalizing Information-Flow Control LibrariesProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993608(15-28)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993608
Patrignani MDevriese DPiessens F(2016)On Modular and Fully-Abstract Compilation2016 IEEE 29th Computer Security Foundations Symposium (CSF)10.1109/CSF.2016.9(17-30)Online publication date: Jun-2016
https://doi.org/10.1109/CSF.2016.9
Iranmanesh ZFallah M(2016)Specification and static enforcement of scheduler-independent noninterference in a middleweight JavaComputer Languages, Systems and Structures10.1016/j.cl.2016.05.00346:C(20-43)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1016/j.cl.2016.05.003
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents