research-article

A Hardware Design Language for Timing-Sensitive Information-Flow Security

Authors:

Andrew C. MyersAuthors Info & Claims

ASPLOS '15: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems

Pages 503 - 516

https://doi.org/10.1145/2694344.2694372

Published: 14 March 2015 Publication History

Abstract

Information security can be compromised by leakage via low-level hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which makes it possible to statically analyze information flow at the hardware level. With SecVerilog, systems can be built with verifiable control of timing channels and other information channels. SecVerilog is Verilog, extended with expressive type annotations that enable precise reasoning about information flow. It also comes with rigorous formal assurance: we prove that SecVerilog enforces timing-sensitive noninterference and thus ensures secure information flow. By building a secure MIPS processor and its caches, we demonstrate that SecVerilog makes it possible to build complex hardware designs with verified security, yet with low overhead in time, space, and HW designer effort.

References

[1]

Icarus Verilog. http://iverilog.icarus.com/.

[2]

O. Acıiçmez. Yet another microarchitectural attack: Exploiting I-cache. In Proc. ACM Workshop on Computer Security Architecture (CSAW '07), pages 11--18, 2007.

Digital Library

[3]

O. Acıiçmez, C. Koç, and J. Seifert. On the power of simple branch prediction analysis. In ASIACCS, pages 312--320, 2007.

Digital Library

[4]

L. Augustsson. Cayenne--a language with dependent types. In Proc. 3rd ACM SIGPLAN Int'l Conf. on Functional Programming (ICFP), pages 239--250, 1998.

Digital Library

[5]

T. H. Austin and C. Flanagan. Efficient purely-dynamic information flow analysis. In Proc. 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), pages 113--124, 2009.

Digital Library

[6]

J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, Apr. 2003. ISBN 0321136160.

Digital Library

[7]

J. Condit, M. Harren, Z. Anderson, D. Gay, and G. C. Necula. Dependent types for low-level programming. In Proc. European Symposium on Programming (ESOP), pages 520--535, 2007.

Digital Library

[8]

B. Coppens, I. Verbauwhede, K. D. Bosschere, and B. D. Sutter. Practical mitigations for timing-based side-channel attacks on modern x86 processors. IEEE Symposium on Security and Privacy, pages 45--60, 2009.

Digital Library

[9]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.

Digital Library

[10]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. CACM, 18(8):453--457, Aug. 1975.

Digital Library

[11]

R. W. Floyd. Assigning meanings to programs. In Proc. Sympos. Appl. Math., volume XIX, pages 19--32, 1967.

[12]

J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy, pages 11--20, Apr. 1982.

[13]

M. Gordon. The semantic challenge of Verilog HDL. In LICS, pages 136--145, 1995.

Digital Library

[14]

R. Grabowski and L. Beringer. Noninterference with dynamic security domains and policies. In Advances in Computer Science -- ASIAN 2009. Information Security and Privacy, pages 54--68, 2009. LNCS 5913.

Digital Library

[15]

D. Gullasch, E. Bangerter, and S. Krenn. Cache games--bringing access-based cache attacks on AES to practice. In IEEE Symposium on Security and Privacy, pages 490--505, 2011.

Digital Library

[16]

M. R. Guthaus, J. S. Ringenberg, D. Ernst, T. M. Austin, T. Mudge, and R. B. Brown. Mibench: A free, commercially representative embedded benchmark suite. In Workload Characterization, 2001. WWC-4. 2001 IEEE International Workshop on, pages 3--14, 2001.

Digital Library

[17]

C. A. R. Hoare. An axiomatic basis for computer programming. CACM, 12(10):576--580, Oct. 1969.

Digital Library

[18]

S. Hunt and D. Sands. On flow-sensitive security types. In POPL 33, pages 79--90, 2006.

Digital Library

[19]

L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. Aura: A programming language for authorization and audit. In Proc. 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 27--38, 2008.

Digital Library

[20]

P. Kocher. Timing attacks on implementations of Diffie--Hellman, RSA, DSS, and other systems. In Advances in Cryptology--CRYPTO'96, Aug. 1996.

Digital Library

[21]

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

Digital Library

[22]

X. Li, V. Kashyap, J. K. Oberg, M. Tiwari, V. R. Rajarathinam, R. Kastner, T. Sherwood, B. Hardekopf, and F. T. Chong. Sapper: A language for hardware-level security policy enforcement. In Proc. 19th Int'l Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 97--112, 2014.

Digital Library

[23]

X. Li, M. Tiwari, J. Oberg, V. Kashyap, F. Chong, T. Sherwood, and B. Hardekopf. Caisson: a hardware description language for secure information flow. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pages 109--120, 2011.

Digital Library

[24]

L. Lourenço and L. Caires. Dependent information flow types. FCT/UNL Technical Report, Oct. 2013.

[25]

A. C. Myers. JFlow: Practical mostly-static information flow control. In POPL 26, pages 228--241, Jan. 1999.

Digital Library

[26]

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

[27]

A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. In Proc. IEEE Symp. on Security and Privacy, pages 165--179, 2011.

Digital Library

[28]

J. Oberg, W. Hu, A. Irturk, M. Tiwari, T. Sherwood, and R. Kastner. Theoretical analysis of gate level information flow tracking. In Proc. 47th Design Automation Conference, pages 244--247, 2010.

Digital Library

[29]

J. Oberg, W. Hu, A. Irturk, M. Tiwari, T. Sherwood, and R. Kastner. Information flow isolation in I2C and USB. In Proc. 48th Design Automation Conference, pages 254--259, 2011.

Digital Library

[30]

D. Osvik, A. Shamir, and E. Tromer. Cache attacks and countermeasures: the case of AES. Topics in Cryptology--CT-RSA 2006, Jan. 2006.

Digital Library

[31]

D. Page. Partitioned cache architecture as a side-channel defense mechanism. In Cryptology ePrint Archive, Report 2005/280, 2005.

[32]

C. Percival. Cache missing for fun and profit. In BSDCan, 2005.

[33]

A. W. Roscoe. CSP and determinism in security modeling. In Proc. IEEE Symp. on Security and Privacy, 1995.

Digital Library

[34]

A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In Proc. 23rd IEEE Computer Security Foundations Symposium (CSF), CSF '10, pages 186--199, 2010.

Digital Library

[35]

A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, Jan. 2003.

Digital Library

[36]

V. Simonet. The Flow Caml System: documentation and user's manual. Technical Report 0282, Institut National de Recherche en Informatique et en Automatique (INRIA), July 2003.

[37]

N. Swamy, J. Chen, and R. Chugh. Enforcing stateful authorization and information flow policies in Fine. In Proc. European Symposium on Programming (ESOP), pages 529--549, 2010.

Digital Library

[38]

N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In Proc. 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 266--278, 2011.

Digital Library

[39]

N. Swamy, B. J. Corcoran, and M. Hicks. Fable: A language for enforcing user-defined security policies. In Proc. IEEE Symp. on Security and Privacy, pages 369--383, 2008.

Digital Library

[40]

M. Tiwari, X. Li, H. M. G. Wassel, F. T. Chong, and T. Sherwood. Execution leases: A hardware-supported mechanism for enforcing strong non-interference. In Micro '09, Dec. 2009.

Digital Library

[41]

M. Tiwari, J. Oberg, X. Li, J. K. Valamehr, T. Levin, B. Hardekopf, R. Kastner, F. T. Chong, and T. Sherwood. Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security. In ISCA'11, June 2011.

Digital Library

[42]

M. Tiwari, H. M. Wassel, B. Mazloom, S. Mysore, F. T. Chong, and T. Sherwood. Complete information flow tracking from the gates up. In ASPLOS XIV, pages 109--120, 2009.

Digital Library

[43]

S. Tse and S. Zdancewic. Run-time principals in information-flow type systems. ACM Transactions on Programming Languages and Systems (TOPLAS), 30(1):6, 2007.

Digital Library

[44]

Z. Wang and R. Lee. Covert and side channels due to processor architecture. In ACSAC '06, pages 473--482, 2006.

Digital Library

[45]

Z. Wang and R. Lee. New cache designs for thwarting software cache-based side channel attacks. In ISCA '07, pages 494--505, 2007.

Digital Library

[46]

H. Xi. Imperative programming with dependent types. In Proc. IEEE Symposium on Logic in Computer Science, pages 375--387, 2000.

Digital Library

[47]

H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, pages 214--227, 1999.

Digital Library

[48]

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

[49]

D. Zhang, A. Askarov, and A. C. Myers. Language-based control and mitigation of timing channels. In Proc. SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pages 99--110, 2012.

Digital Library

[50]

D. Zhang, Y. Wang, G. E. Suh, and A. C. Myers. A hardware design language for efficient control of timing channels. Technical report, Cornell University, Apr. 2014. http://hdl.handle.net/1813/36274.

[51]

L. Zheng and A. C. Myers. Dynamic security labels and static information flow control. Int'l J. of Information Security, 6(2--3), Mar. 2007.

Digital Library

Cited By

Saravanan RPudukotai Dinakarrao S(2024)Exploring Coverage Metrics in Hardware Fuzzing: A Comprehensive AnalysisProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3660386(240-245)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3660386
Goli MDrechsler R(2024)Early SoCs Information Flow Policies Validation Using SystemC-Based Virtual Prototypes at the ESLACM Transactions on Embedded Computing Systems10.1145/354478023:5(1-20)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3544780
Ryan KGregoire MSturton C(2023)SEIF: Augmented Symbolic Execution for Information Flow in Hardware DesignsProceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy10.1145/3623652.3623666(1-9)Online publication date: 29-Oct-2023
https://dl.acm.org/doi/10.1145/3623652.3623666
Show More Cited By

Index Terms

A Hardware Design Language for Timing-Sensitive Information-Flow Security
1. Hardware
  1. Electronic design automation
    1. Hardware description languages and compilation

Recommendations

A Hardware Design Language for Timing-Sensitive Information-Flow Security
ASPLOS '15

Information security can be compromised by leakage via low-level hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which ...
A Hardware Design Language for Timing-Sensitive Information-Flow Security
ASPLOS'15

Information security can be compromised by leakage via low-level hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which ...
Language-based control and mitigation of timing channels
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

We propose a new language-based approach to mitigating timing channels. In this language, well-typed programs provably leak only a bounded amount of information over time through external timing channels. By incorporating mechanisms for predictive ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPLOS '15: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems

March 2015

720 pages

ISBN:9781450328357

DOI:10.1145/2694344

General Chairs:
Ozcan Ozturk
Bilkent University, Turkey
,
Kemal Ebcioglu
Global Supercomputing, USA
,
Program Chair:
Sandhya Dwarkadas
University of Rochester, USA

ACM SIGPLAN Notices Volume 50, Issue 4
ASPLOS '15
April 2015
676 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775054
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents
ACM SIGARCH Computer Architecture News Volume 43, Issue 1
ASPLOS'15
March 2015
676 pages
ISSN:0163-5964
DOI:10.1145/2786763
Editor:
Doug DeGroot
acm dot org
Issue’s Table of Contents

Copyright © 2015 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]

Sponsors

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 March 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ASPLOS '15

Sponsor:

ASPLOS '15: Architectural Support for Programming Languages and Operating Systems

March 14 - 18, 2015

Istanbul, Turkey

Acceptance Rates

ASPLOS '15 Paper Acceptance Rate 48 of 287 submissions, 17%;

Overall Acceptance Rate 535 of 2,713 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

187
Total Citations
View Citations
1,148
Total Downloads

Downloads (Last 12 months)108
Downloads (Last 6 weeks)10

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Saravanan RPudukotai Dinakarrao S(2024)Exploring Coverage Metrics in Hardware Fuzzing: A Comprehensive AnalysisProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3660386(240-245)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3660386
Goli MDrechsler R(2024)Early SoCs Information Flow Policies Validation Using SystemC-Based Virtual Prototypes at the ESLACM Transactions on Embedded Computing Systems10.1145/354478023:5(1-20)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.1145/3544780
Ryan KGregoire MSturton C(2023)SEIF: Augmented Symbolic Execution for Information Flow in Hardware DesignsProceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy10.1145/3623652.3623666(1-9)Online publication date: 29-Oct-2023
https://dl.acm.org/doi/10.1145/3623652.3623666
Wang ZMohr Gvon Gleissenthall KReineke JGuarnieri MMeng WJensen CCremers CKirda E(2023)Specification and Verification of Side-channel Security for Open-source Processors via Leakage ContractsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623192(2128-2142)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623192
Luo MXiong WLee GLi YYang XZhang ATian YLee HSuh G(2023)AutoCAT: Reinforcement Learning for Automated Exploration of Cache-Timing Attacks2023 IEEE International Symposium on High-Performance Computer Architecture (HPCA)10.1109/HPCA56546.2023.10070947(317-332)Online publication date: Feb-2023
https://doi.org/10.1109/HPCA56546.2023.10070947
Baty MWilke PHiet GFontaine ATrieu A(2023)A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00029(372-387)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00029
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582
Ahmad BLiu WCollini LPearce HFung JValamehr JBidmeshki MSapiecha PBrown SChakrabarty KKarri RTan BMitra TYoung EXiong J(2022)Don't CWEAT ItProceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design10.1145/3508352.3549369(1-9)Online publication date: 30-Oct-2022
https://dl.acm.org/doi/10.1145/3508352.3549369
Zhou XXu ZWang CGao MSalapura VZahran MChong FTang L(2022)PPMLACProceedings of the 49th Annual International Symposium on Computer Architecture10.1145/3470496.3527392(87-101)Online publication date: 18-Jun-2022
https://dl.acm.org/doi/10.1145/3470496.3527392
Pearce HAhmad BTan BDolan-Gavitt BKarri R(2022)Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833571(754-768)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833571
Show More Cited By

View Options

Get Access

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 Table of Contents