The Community for Technology Leaders
RSS Icon
Issue No.11 - Nov. (2013 vol.62)
pp: 2292-2307
Karthik Pattabiraman , University of British Columbia, Vancouver
Nithin M. Nakka , Nexstest Systems, San Jose
Zbigniew T. Kalbarczyk , University of Illinois at Urbana-Champaign, Urbana
Ravishankar K. Iyer , University of Illinois at Urbana-Champaign, Urbana
This paper introduces SymPLFIED, a program-level framework that allows specification of arbitrary error detectors and the verification of their efficacy against hardware errors. SymPLFIED comprehensively enumerates all transient hardware errors in registers, memory, and computation (expressed symbolically as value errors) that potentially evade detection and cause program failure. The framework uses symbolic execution to abstract the state of erroneous values in the program and model checking to comprehensively find all errors that evade detection. We demonstrate the use of SymPLFIED on a widely deployed aircraft collision avoidance application, tcas. Our results show that the SymPLFIED framework can be used to uncover hard-to-detect catastrophic cases caused by transient errors in programs that may not be exposed by random fault injection-based validation. Further, the errors exposed by the framework help us formulate a set of error detectors for the application to avoid the catastrophic case and other incorrect outcomes.
Registers, Detectors, Hardware, Assembly, Computational modeling, Transient analysis,error detection, Fault injection, model checking
Karthik Pattabiraman, Nithin M. Nakka, Zbigniew T. Kalbarczyk, Ravishankar K. Iyer, "SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework", IEEE Transactions on Computers, vol.62, no. 11, pp. 2292-2307, Nov. 2013, doi:10.1109/TC.2012.219
[1] M. Hiller, A. Jhumka, and N. Suri, "On the Placement of Software Mechanisms for Detection of Data Errors," Proc. Int'l Conf. Dependable Systems and Networks (DSN '02), pp. 135-144, 2002.
[2] K. Pattabiraman, Z. Kalbarczyk, and R.K. Iyer, "Automated Derivation of Application-Aware Error Detectors Using Static Analysis," Proc. 13th Int'l On-Line Testing Symp., 2007.
[3] W. Gu, Z. Kalbarczyk, R.K. Iyer, and Z. Yang, "Characterization of Linux Kernel Behavior under Errors," Proc. Int'l Conf. Dependable Systems and Networks (DSN '03), pp. 459-468, 2003.
[4] J. Arlat et al., "Fault Injection for Dependability Validation: A Methodology and Some Applications," IEEE Trans. Software Eng., vol. 16, no. 2, pp. 166-182, Feb. 1990.
[5] H. Madeira, J. Carreira, and J.G. Silva, "Injection of Faults in Complex Computers," Proc. IEEE Workshop Evaluation Techniques for Dependable Systems, Oct. 1995.
[6] D. Cyrluk, "Microprocessor Verification in PVS: A Methodology and Simple Example," Technical Report SRI-CSL-93-12, SRI Int'l, 1993.
[7] R.S. Boyer and J S. Moore, "Program Verification," J. Automated Reasoning, vol. 1, pp. 17-23, 1985.
[8] U. Krautz et al., "Evaluating Coverage of Error Detection Logic for Soft Errors Using Formal Methods," Proc. Conf. Design, Automation and Test in Europe (DATE '06), 2006.
[9] S.A. Seshia, W. Li, and S. Mitra, "Verification-Guided Soft Error Resilience," Proc. Conf. Design, Automation and Test in Europe (DATE '07), 2007.
[10] A. Arora and S.S. Kulkarni, "Detectors and Correctors: A Theory of Fault-Tolerance Components," Proc. Int'l Conf. Distributed Computing Systems, pp. 436-443, 1998.
[11] B. Nicolescu, N. Gorse, Y. Savaria, E.M. Aboulhamid, and R. Velazco, "On the Use of Model Checking for the Verification of a Dynamic Signature Monitoring Approach," IEEE Trans. Nuclear Science, vol. 52, no. 5, pp. 1555-1561, Oct. 2005.
[12] F. Perry et al., "Fault-Tolerant Typed Assembly Language," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI '07), 2007.
[13] M.L. Matthew and D. Walker, "Faulty Logic: Reasoning about Fault Tolerant Programs," Proc. European Symp. Programming (ESOP '10), 2010.
[14] J.C. King, "Symbolic Execution and Program Testing," Comm. ACM, vol. 19, no. 7, pp. 385-394, July 1976.
[15] W. Bush et al., "A Static Analyzer for Finding Dynamic Programming Errors," Software: Practice and Experience, vol. 30, no. 7, pp. 775-802, 2000.
[16] D. Larson and R. Hahnle, "Symbolic Fault Injection," Proc. Int'l Verification Workshop (VERIFY '07), vol. 259, pp. 85-103, 2007.
[17] M. Clavel, S. Eker, P. Lincoln, and J. Meseguer, "Principles of Maude," Proc. First Int'l Workshop Rewriting Logic and Its Applications, 1996.
[18] E. Clarke, A. Biere, R. Raimi, and Y. Zhu, "Bounded Model Checking Using Satisfiability Solving," Formal Methods in System Design, vol. 19, pp. 7-34, 2001.
[19] M. Clavel et al., "The Maude Formal Tool Environment," Proc. Second Int'l Conf. Algebra and Coalgebra in Computer Science, pp. 173-178, Aug. 2007.
[20] M. Hutchins, H. Foster, T. Goradia, and T. Ostrand, "Experiments on the Effectiveness of Dataflow- and Control Flow-Based Test Adequacy Criteria," Proc. Int'l Conf. Software Eng. (ICSE '94), pp. 191-200, 1994.
[21] D. Burger and T.M. Austin, "The SimpleScalar Tool Set, Version 2.0," ACM SIGARCH Computer Architecture News, vol. 25, no. 3, pp. 13-25, 1997.
[22] J. Lygeros and N.A. Lynch, "On the Formal Verification of the TCAS Conflict Resolution Algorithms," Proc. IEEE 36th Conf. Decision and Control, pp. 1829-1834, 1997.
[23] Federal Aviation Administration, "TCAS 2 Collision Avoidance System (CAS) System Requirements Specification," http://adsb. tc.faa.govTCAS.htm, 1993.
[24] N. Nakka, Z. Kalbarczyk, R.K. Iyer, and J. Xu., "An Architectural Framework for Providing Reliability and Security Support," Proc. Int'l Conf. Dependable Systems and Networks (DSN '04), pp. 585-594, 2004.
[25] B.A. Kuperman, C.E. Brodley, H. Ozdoganoglu, T.N. Vijaykumar, and A. Jalote, "Detection and Prevention of Stack Buffer Overflow Attacks," Comm. ACM, vol. 18, no. 11, pp. 50-56, Nov. 2005.
[26] J.L. Hennessey and D.A. Patterson, Computer Organization and Design: The Hardware-Software Interface. Morgan Kauffman, 2011.
[27] K. Pattabiraman, N. Nakka, Z. Kalbarczyk, and R.K. Iyer, "SymPLFIED: Symbolic Program Level Fault Injection and Error Detection," Technical Report UILU-ENG-08-2205, Univ. of Illinois at Urbana-Champaign, Jan. 2008.
41 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool