Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

Security-critical communications devices must be evaluated to the highest possible standards before they can be deployed. This process includes tracing potential information flow through the device's electronic circuitry, for each of the device's operating modes. Increasingly, however, security functionality is being entrusted to embedded software running on microprocessors within such devices, so new strategies are needed for integrating information flow analyses of embedded program code with hardware analyses. Here we show how standard compiler principles can augment high-integrity security evaluations to allow seamless tracing of information flow through both the hardware and software of embedded systems. This is done by unifying input/output statements in embedded program execution paths with the hardware pins they access, and by associating significant software states with corresponding operating modes of the surrounding electronic circuitry.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Marco Avvenuti , Cinzia Bernardeschi , Nicoletta De Francesco, Java bytecode verification for secure information flow, ACM SIGPLAN Notices, v.38 n.12, December 2003 [doi>10.1145/966051.966055]
• 3: Karl J. Ottenstein , Robert A. Ballance , Arthur B. MacCabe, The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.257-271, June 1990, White Plains, New York, United States [doi>10.1145/93542.93578]
• 4: K. Banks. Tips for checking schematics. Embedded Systems, 16(6):36--38, June 2003.
• 5: H. Bar-El, H. Choukri, D. Naccache, M. Tunstall, and C. Whelan. The sorcerer's apprentice guide to fault attacks. Proceedings of the IEEE, 94(2):370--382, February 2006.
• 6: D. Clark, C. Hankin, and S. Hunt. Information flow for ALGOL-like languages. Computer Languages, 28(1):3--28, April 2002.
• 7: A. W. Dent and J. Malone-Lee. The physically observable security of signature schemes. In N. P. Smart, editor, Cryptography and Coding -- Tenth IMA International Conference, volume 3796 of Lecture Notes in Computer Science, pages 220--232, Cirencester, United Kingdom, 19--21 December 2005. Springer-Verlag, Berlin.
• 8: Jeanne Ferrante , Karl J. Ottenstein , Joe D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.319-349, July 1987 [doi>10.1145/24039.24041]
• 9: Susan Horwitz , Thomas Reps, The use of program dependence graphs in software engineering, Proceedings of the 14th international conference on Software engineering, p.392-411, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143156]
• 10: Rajeev Joshi , K. Rustan M. Leino, A semantic approach to secure information flow, Science of Computer Programming, v.37 n.1-3, p.113-138, May 2000 [doi>10.1016/S0167-6423(99)00024-6]
• 11: Volkmar Lotz , Volker Kessler , Georg H. Walter, A Formal Security Model for Microprocessor Hardware, IEEE Transactions on Software Engineering, v.26 n.8, p.702-712, August 2000 [doi>10.1109/32.879809]
• 12: A. Mahalingam, B. P. Butz, and M. Duarte. An intelligent circuit analysis module to analyze student queries in the Universal Virtual Laboratory. In W. Oakes, D. Voltmer, and C. Yokomoto, editors, Proceedings of the 35th ASEE/IEEE Frontiers in Education Conference (FIE'05), pages F4E-1-F4E-6, Indianapolis, USA, 19--22 October 2005. Institute of Electrical and Electronics Engineers, New Jersey, USA.
• 13: T. McComb and L. P. Wildman. SIFA: A tool for evaluation of high-grade security devices. In C. Boyd and J. Nieto, editors, Proceedings of the Tenth Australasian Conference on Information Security and Privacy (ACISP 2005), volume 3574 of Lecture Notes in Computer Science, pages 230--241, Brisbane, Australia, 4--6 July 2005. Springer-Verlag, Berlin.
• 14: T. McComb and L. P. Wildman. Verifying abstract information flow properties in fault tolerant security devices. In Z. Liu and J. He, editors, Proceedings of the Eighth International Conference on Formal Engineering Methods (ICFEM 2006), volume 4260 of Lecture Notes in Computer Science, pages 621--638, Macao, China, 1--3 November 2006. Springer-Verlag, Berlin.
• 15: Andrew C. Myers , Andrei Sabelfeld , Steve Zdancewic, Enforcing robust declassification and qualified robustness, Journal of Computer Security, v.14 n.2, p.157-196, April 2006
• 16: Kevin R. O'Neill , Michael R. Clarkson , Stephen Chong, Information-Flow Security for Interactive Programs, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.190-201, July 05-07, 2006 [doi>10.1109/CSFW.2006.16]
• 17: M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
• 18: Andrew Rae , Colin Fidge, Information Flow Analysis for Fail-Secure Devices, The Computer Journal, v.48 n.1, p.17-26, January 2005 [doi>10.1093/comjnl/bxh056]
• 19: A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):1--15, January 2003.
• 20: B. Schlich, M. Rohrbach, M. Weber, and S. Kowalewski. Model checking software for microcontrollers. Technical Report AIB-2006-11, Department of Computer Science, RWTH Aachen University, Germany, 2006.
• 21: Gregor Snelting , Torsten Robschink , Jens Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.4, p.410-457, October 2006 [doi>10.1145/1178625.1178628]
• 22: The Common Criteria Project Sponsoring Organisations. Common Criteria for Information Technology Security Evaluation. International Organization for Standardization, Geneva, August 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

General Terms:
Security, Verification

Keywords:
communications devices, embedded software, information security evaluation