More Web Proxy on the site http://driver.im/

research-article

Addressing covert termination and timing channels in concurrent information flow systems

Authors:

Alejandro Russo,

John C. Mitchell,

David MaziéresAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 9

Pages 201 - 214

https://doi.org/10.1145/2398856.2364557

Published: 09 September 2012 Publication History

Abstract

When termination of a program is observable by an adversary, confidential information may be leaked by terminating accordingly. While this termination covert channel has limited bandwidth for sequential programs, it is a more dangerous source of information leakage in concurrent settings. We address concurrent termination and timing channels by presenting a dynamic information-flow control system that mitigates and eliminates these channels while allowing termination and timing to depend on secret values. Intuitively, we leverage concurrency by placing such potentially sensitive actions in separate threads. While termination and timing of these threads may expose secret values, our system requires any thread observing these properties to raise its information-flow label accordingly, preventing leaks to lower-labeled contexts. We implement this approach in a Haskell library and demonstrate its applicability by building a web server that uses information-flow control to restrict untrusted web applications.

References

[1]

J. Agat. Transforming out timing leaks. In Proc. ACM Symp. on Principles of Programming Languages, pages 40--53, Jan. 2000.

Digital Library

[2]

A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. Termination-insensitive noninterference leaks more than just a bit. In Proc. of the 13th ESORICS. Springer-Verlag, 2008.

Digital Library

[3]

A. Askarov, D. Zhang, and A. C. Myers. Predictive black-box mitigation of timing channels. In Proc. of the 17th ACM CCS. ACM, 2010.

Digital Library

[4]

G. Barthe, T. Rezk, and M. Warnier. Preventing timing leaks through transactional branching instructions. Electron. Notes Theor. Comput. Sci., 153, May 2006.

Digital Library

[5]

G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld. Security of multithreaded programs by compilation. In Proc. European Symp. on Research in Computer Security, pages 2--18, Sept. 2007.

Digital Library

[6]

A. Bortz and D. Boneh. Exposing private information by timing web applications. In Proc. of the 16th World Wide Web. ACM, 2007.

Digital Library

[7]

Boudol and Castellani. Noninterference for concurrent programs. In Proc. ICALP'01, volume 2076 of LNCS. Springer-Verlag, July 2001.

Digital Library

[8]

G. Boudol and I. Castellani. Non-interference for concurrent programs and thread systems. Theoretical Computer Science, 281(1), June 2002.

Digital Library

[9]

D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236--243, May 1976.

Digital Library

[10]

D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504--513, 1977.

Digital Library

[11]

D. Devriese and F. Piessens. Noninterference through secure multi-execution. In Proc. of the 2010 IEEE Symposium on Security and Privacy, SP '10. IEEE Computer Society, 2010.

Digital Library

[12]

D. Devriese and F. Piessens. Information flow enforcement in monadic libraries. In Proc. of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation. ACM, 2011.

Digital Library

[13]

P. Efstathopoulos, M. Krohn, S. VanDeBogart, C. Frey, D. Ziegler, E. Kohler, D. Maziéres, F. Kaashoek, and R. Morris. Labels and event processes in the asbestos operating system. In Proc. of the twentieth ACM symp. on Operating systems principles, SOSP '05. ACM, 2005.

Digital Library

[14]

M. Felleisen. The theory and practice of first-class prompts. In Proc. of the 15th ACM SIGPLAN-SIGACT Symp. on Principles of programming languages, pages 180--190. ACM, 1988.

Digital Library

[15]

E. W. Felten and M. A. Schneider. Timing attacks on web privacy. In Proc. of the 7th ACM conference on Computer and communications security, CCS '00. ACM, 2000.

Digital Library

[16]

G. L. Guernic. Automaton-based confidentiality monitoring of concurrent programs. In Proc. of the 20th IEEE Computer Security Foundations Symposium, CSF '07. IEEE Computer Society, 2007.

Digital Library

[17]

H. Handschuh and H. M. Heys. A timing attack on RC5. In Proc. of the Selected Areas in Cryptography. Springer-Verlag, 1999.

Digital Library

[18]

D. Hedin and A. Sabelfeld. A perspective on information-flow control. In Proc. of the 2011 Marktoberdorf Summer School. IOS Press, 2011.

[19]

D. Hedin and D. Sands. Timing aware information flow security for a javacard-like bytecode. Elec. Notes Theor. Comput. Sci., 141, 2005.

Digital Library

[20]

M. Hennessy and J. Riely. Information flow vs. resource access in the asynchronous pi-calculus. ACM Trans. Program. Lang. Syst., 24(5), Sept. 2002.

Digital Library

[21]

K. Honda and N. Yoshida. A uniform type structure for secure information flow. ACM Trans. Program. Lang. Syst., Oct. 2007.

Digital Library

[22]

K. Honda, V. T. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In Proc. of the 9th European Symposium on Programming Languages and Systems. Springer-Verlag, 2000.

Digital Library

[23]

M. Huisman, P. Worah, and K. Sunesen. A temporal logic characterisation of observational determinism. In Proc. IEEE Computer Sec. Foundations Workshop, July 2006.

Digital Library

[24]

M. Jaskelioff and A. Russo. Secure multi-execution in Haskell. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS. Springer-Verlag, June 2011.

Digital Library

[25]

S. P. Jones, A. Gordon, and S. Finne. Concurrent Haskell. In Proc. of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1996.

Digital Library

[26]

V. Kashyap, B. Wiedermann, and B. Hardekopf. Timing- and termination-sensitive secure information flow: Exploring a new approach. In Proc. of IEEE Symposium on Sec. and Privacy. IEEE, 2011.

Digital Library

[27]

N. Kobayashi. Type-based information flow analysis for the π-calculus. Acta Inf., 42(4), Dec. 2005.

Digital Library

[28]

P. C. Kocher. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Proc. of the 16th CRYPTO. Springer-Verlag, 1996.

Digital Library

[29]

B. Köpf and H. Mantel. Eliminating implicit information leaks by transformational typing and unification. In Formal Aspects in Security and Trust, Third International Workshop (FAST'05), volume 3866 of LNCS. Springer-Verlag, July 2006.

Digital Library

[30]

B.W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10):613--615, 1973.

Digital Library

[31]

P. Li and S. Zdancewic. Encoding Information Flow in Haskell. In CSFW '06: Proc. of the 19th IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 2006.

Digital Library

[32]

P. Li and S. Zdancewic. Arrows for secure information flow. Theoretical Computer Science, 411(19):1974--1994, 2010.

Digital Library

[33]

S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In In Proc. of the 22nd ACM Symposium on Principles of Programming Languages. ACMPress, 1995.

Digital Library

[34]

H. Mantel, H. Sudbrock, and T. Krausser. Combining different proof techniques for verifying information flow security. In Proc. of the 16th international conference on Logic-based program synthesis and transformation, LOPSTR'06. Springer-Verlag, 2007.

Digital Library

[35]

M. D. Mcilroy and J. A. Reeds. Multilevel security in the unix tradition. Software Practice and Experience, 22:673--694, 1992.

Digital Library

[36]

J. Morgenstern and D. R. Licata. Security-typed programming within dependently typed programming. In Proc. of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM, 2010.

Digital Library

[37]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proc. of the 16th ACM Symp. on Operating Systems Principles, pages 129--142, 1997.

Digital Library

[38]

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

[39]

F. Pottier. A simple view of type-secure information flow in the π-calculus. In In Proc. of the 15th IEEE Computer Security Foundations Workshop, pages 320--330, 2002.

Digital Library

[40]

A. Russo and A. Sabelfeld. Securing interaction between threads and the scheduler. In Proc. IEEE Computer Sec. Foundations Workshop, pages 177--189, July 2006.

Digital Library

[41]

A. Russo and A. Sabelfeld. Security for multithreaded programs under cooperative scheduling. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics (PSI), LNCS. Springer-Verlag, June 2006.

Digital Library

[42]

A. Russo, J. Hughes, D. Naumann, and A. Sabelfeld. Closing internal timing channels by transformation. In Proc. of Asian Computing Science Conference, LNCS. Springer-Verlag, Dec. 2006.

Digital Library

[43]

A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. In Proc. ACM SIGPLAN Symposium on Haskell, pages 13--24. ACM Press, Sept. 2008.

Digital Library

[44]

A. Sabelfeld. The impact of synchronisation on secure information flow in concurrent programs. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics, volume 2244 of LNCS, pages 225--239. Springer-Verlag, July 2001.

Digital Library

[45]

A. Sabelfeld and H. Mantel. Static confidentiality enforcement for distributed programs. In Proc. Symp. on Static Analysis, volume 2477 of LNCS, pages 376--394. Springer-Verlag, Sept. 2002.

Digital Library

[46]

A. Sabelfeld and A. Russo. 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. Springer-Verlag, June 2009.

Digital Library

[47]

A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded programs. In Proc. IEEE Computer Sec. Foundations Workshop, pages 200--214, July 2000.

Digital Library

[48]

V. Simonet. The Flow Caml system. Software release at http://cristal.inria.fr/~simonet/soft/flowcaml/, July 2003.

[49]

Smith. Probabilistic noninterference through weak probabilistic bisimulation. In Proc. IEEE Computer Sec. Foundations Workshop, pages 3--13, 2003.

[50]

G. Smith. A new type system for secure information flow. In Proc. IEEE Computer Sec. Foundations Workshop, June 2001.

Digital Library

[51]

G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. ACM Symp. on Principles of Programming Languages, pages 355--364, Jan. 1998.

Digital Library

[52]

D. Stefan, A. Russo, J. C. Mitchell, and D. Maziéres. Flexible dynamic information flow control in Haskell. In Haskell Symposium. ACM SIGPLAN, September 2011.

Digital Library

[53]

T. Terauchi. A type system for observational determinism. In Proc. of the 2008 21st IEEE Computer Security Foundations Symposium, pages 287--300. IEEE Computer Society, 2008.

Digital Library

[54]

T. C. Tsai, A. Russo, and J. Hughes. A library for secure multi-threaded information flow in Haskell. In Proc. IEEE Computer Sec. Foundations Symposium, July 2007.

Digital Library

[55]

D. Volpano and G. Smith. Eliminating covert flows with minimum typings. In Proc. of the 10th IEEE workshop on Computer Security Foundations, CSFW '97. IEEE Computer Society, 1997.

Digital Library

[56]

D. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. J. Computer Security, 7(2-3), Nov. 1999.

Digital Library

[57]

W. H. Wong. Timing attacks on RSA: revealing your secrets through the fourth dimension. Crossroads, 11, May 2005.

Digital Library

[58]

S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In Proc. IEEE Computer Sec. Foundations Workshop, pages 29--43, June 2003.

[59]

N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Maziéres. Making information flow explicit in histar. In Proc. of the 7th USENIX Symp. on Operating Systems Design and Implementation. USENIX, 2006.

Digital Library

[60]

D. Zhang, A. Askarov, and A. C. Myers. Predictive mitigation of timing channels in interactive systems. In Proc. of the 18th ACM CCS. ACM, 2011.

Digital Library

[61]

D. Zhang, A. Askarov, and A. C. Myers. Language-based control and mitigation of timing channels. In Proc. of PLDI. ACM, 2012.

Digital Library

Cited By

Wei SHarris AZhu YRamrakhyani PLin CTiwari M(2024)Tail Victims in Termination Timing Channel Defenses Beyond Cryptographic Kernels2024 International Symposium on Secure and Private Execution Environment Design (SEED)10.1109/SEED61283.2024.00012(11-22)Online publication date: 16-May-2024
https://doi.org/10.1109/SEED61283.2024.00012
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
Algehed MBernardy JHriţcu C(2021)Dynamic IFC Theorems for Free!2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00005(1-14)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00005
Show More Cited By

Index Terms

Addressing covert termination and timing channels in concurrent information flow systems

Recommendations

Addressing covert termination and timing channels in concurrent information flow systems
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

When termination of a program is observable by an adversary, confidential information may be leaked by terminating accordingly. While this termination covert channel has limited bandwidth for sequential programs, it is a more dangerous source of ...
Covert channels in privacy-preserving identification systems
CCS '07: Proceedings of the 14th ACM conference on Computer and communications security

We examine covert channels in privacy-enhanced mobile identification devices where the devices uniquely identify themselves to an authorized verifier. Such devices (e.g. RFID tags) are increasingly commonplace in hospitals and many other environments. ...
Detecting covert timing channels: an entropy-based approach
CCS '07: Proceedings of the 14th ACM conference on Computer and communications security

The detection of covert timing channels is of increasing interest in light of recent practice on the exploitation of covert timing channels over the Internet. However, due to the high variation in legitimate network traffic, detecting covert timing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 9

ICFP '12

September 2012

368 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2398856

Issue’s Table of Contents

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
September 2012
392 pages
ISBN:9781450310543
DOI:10.1145/2364527
General Chair:
Peter Thiemann
University of Freiburg, Germany
,
Program Chair:
Robby Findler
Northwestern University, USA

Copyright © 2012 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: 09 September 2012

Published in SIGPLAN Volume 47, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
463
Total Downloads

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

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wei SHarris AZhu YRamrakhyani PLin CTiwari M(2024)Tail Victims in Termination Timing Channel Defenses Beyond Cryptographic Kernels2024 International Symposium on Secure and Private Execution Environment Design (SEED)10.1109/SEED61283.2024.00012(11-22)Online publication date: 16-May-2024
https://doi.org/10.1109/SEED61283.2024.00012
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
Algehed MBernardy JHriţcu C(2021)Dynamic IFC Theorems for Free!2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00005(1-14)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00005
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Ghosal SShyamasundar RNarendra Kumar N(2019)Compile-Time Security Certification of Imperative Programming LanguagesE-Business and Telecommunications10.1007/978-3-030-34866-3_8(159-182)Online publication date: 13-Nov-2019
https://doi.org/10.1007/978-3-030-34866-3_8
Alpernas KFlanagan CFouladi SRyzhyk LSagiv MSchmitz TWinstein K(2018)Secure serverless computing using dynamic information flow controlProceedings of the ACM on Programming Languages10.1145/32764882:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276488
Ferraiuolo AZhao MMyers ASuh GLie DMannan MBackes MWang X(2018)HyperFlowProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243743(1583-1600)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243743
Shu RWang PGorski III SAndow BNadkarni ADeshotels LGionta JEnck WGu X(2016)A Study of Security Isolation TechniquesACM Computing Surveys10.1145/298854549:3(1-37)Online publication date: 12-Oct-2016
https://dl.acm.org/doi/10.1145/2988545
Rahmati AFernandes EPrakash A(2016)Applying the Opacified Computation Model to Enforce Information Flow Policies in IoT Applications2016 IEEE Cybersecurity Development (SecDev)10.1109/SecDev.2016.031(88-93)Online publication date: Nov-2016
https://doi.org/10.1109/SecDev.2016.031
Rafnsson WGarg DSabelfeld A(2016)Progress-Sensitive Security for SPARKProceedings of the 8th International Symposium on Engineering Secure Software and Systems - Volume 963910.1007/978-3-319-30806-7_2(20-37)Online publication date: 6-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-319-30806-7_2
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 Publication

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