Farid Molazem Tabrizi and Karthik Pattabiraman, ACM Transactions on Embedded Computing Systems (TECS). [ PDF ]. Awarded best paper of TECS 2020 (ECE Story). Received significant news coverage (below).
(This paper supercedes our ACSAC’16 paper.)
Continue reading
Tag Archives: formal
Design-Level and Code-Level Security Analysis of IoT Devices
Comments Off on Design-Level and Code-Level Security Analysis of IoT Devices
Filed under papers
SymPLFIED: Symbolic Program Level Fault Injection and Error Detection Framework
Karthik Pattabiraman, Nithin Nakka, Zbigniew Kalbarczyk and Ravishankar Iyer, To appear in the IEEE Transactions on Computers (TC). November 2013. [PDF file].
Continue reading
Comments Off on SymPLFIED: Symbolic Program Level Fault Injection and Error Detection Framework
Filed under papers
Formal Diagnosis of Hardware Transient Errors in Programs
Layali Rashid, Karthik Pattabiraman and Sathish Gopalakrishnan, Workshop on Silicon Errors in Logic, System Effects (SELSE), 2010. [ PDF File ][ Talk Slides ]
Continue reading
Comments Off on Formal Diagnosis of Hardware Transient Errors in Programs
Filed under papers
Talk: Formal methods for Fault and Attack Injection in Applications
Talk given at LAAS, CNRS, Toulouse, France. Feb 19th, 2010.
[ Slides in PDF ]
Continue reading
Comments Off on Talk: Formal methods for Fault and Attack Injection in Applications
Filed under Talks
Discovering Application-level Insider Attacks Using Symbolic Execution
Karthik Pattabiraman, Zbigniew Kalbarczyk and Ravishankar Iyer, Proceedings of the IFIP International Conference on Information Security (SEC), 2009.[ PDF File | Talk ]
You can find the technical report version of the paper here.
Continue reading
Filed under papers
SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework
Karthik Pattabiraman, Nithin Nakka, Zbigniew Kalbarczyk and Ravishankar Iyer, Proceedings of the International Conference on Dependable Systems and Networks (DSN), 2008.
This paper won the William C. Carter award for the best paper at the conference
[ PDF File | Talk ]
You can find the tech report for the conference paper here.
Abstract: This paper introduces SymPLFIED, a program-level framework which 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 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 corner cases caused by transient errors in programs that may not be exposed by random fault-injection based validation.
The Coordinated Science Lab at UIUC did an article about this paper
Comments Off on SymPLFIED: Symbolic Program-Level Fault Injection and Error Detection Framework
Filed under papers
