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

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.
3. O. Acıiçmez, C. Koç, and J. Seifert. On the power of simple branch prediction analysis. In ASIACCS, pages 312--320, 2007.
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.
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.
6. J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, Apr. 2003. ISBN 0321136160.
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.
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.
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.
10. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. CACM, 18(8):453--457, Aug. 1975.
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.
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.
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.
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.
17. C. A. R. Hoare. An axiomatic basis for computer programming. CACM, 12(10):576--580, Oct. 1969.
18. S. Hunt and D. Sands. On flow-sensitive security types. In POPL 33, pages 79--90, 2006.
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.
20. P. Kocher. Timing attacks on implementations of Diffie--Hellman, RSA, DSS, and other systems. In Advances in Cryptology--CRYPTO'96, Aug. 1996.
21. B. W. Lampson. A note on the confinement problem. Comm. of the ACM, 16(10):613--615, Oct. 1973.
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.
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.
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.
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.
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.
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.
30. D. Osvik, A. Shamir, and E. Tromer. Cache attacks and countermeasures: the case of AES. Topics in Cryptology--CT-RSA 2006, Jan. 2006.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
44. Z. Wang and R. Lee. Covert and side channels due to processor architecture. In ACSAC '06, pages 473--482, 2006.
45. Z. Wang and R. Lee. New cache designs for thwarting software cache-based side channel attacks. In ISCA '07, pages 494--505, 2007.
46. H. Xi. Imperative programming with dependent types. In Proc. IEEE Symposium on Logic in Computer Science, pages 375--387, 2000.
47. H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, pages 214--227, 1999.
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.
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.

Index Terms

• Hardware

  • Electronic design automation

    • Hardware description languages and compilation