TY - GEN
T1 - Reasoning about control flow in the presence of transient faults
AU - Perry, Frances
AU - Walker, David
N1 - Funding Information:
This research is funded in part by NSF award CNS-0627650 and a Microsoft graduate fellowship. We would like to thanks Andrew Appel, David August, George Reis and Neil Vachharajani for many enlightening discussions on transient faults, harware mechanisms and fault tolerance.
PY - 2008
Y1 - 2008
N2 - A transient fault is a temporary, one-time event that causes a change in state or erroneous signal transfer in a digital circuit. These faults do not cause permanent damage, but when they strike conventional processors, they may result in incorrect program execution. While detecting and correcting faults in first-order data may be accomplished relatively easily by adding redundancy, protecting against faults during control flow transfers is substantially more difficult. This paper analyzes the problem of maintaining the control-flow integrity of a program in the face of transient faults from a formal theoretical perspective. More specifically, we augment the operational semantics of an idealized assembly language with additional rules that model erroneous control-flow transfers. Next, we explain a strategy for detecting control-flow errors based on previous work by Oh [10] and Reis [15]. In order to reason about the correctness of the strategy relative to our fault model, we develop a new assembly-level type system designed to guarantee that any control flow transfer to an incorrect block will be caught before control leaves that block. The key technical result of the paper is a rigorous proof of this fundamental control-flow property for well-typed programs.
AB - A transient fault is a temporary, one-time event that causes a change in state or erroneous signal transfer in a digital circuit. These faults do not cause permanent damage, but when they strike conventional processors, they may result in incorrect program execution. While detecting and correcting faults in first-order data may be accomplished relatively easily by adding redundancy, protecting against faults during control flow transfers is substantially more difficult. This paper analyzes the problem of maintaining the control-flow integrity of a program in the face of transient faults from a formal theoretical perspective. More specifically, we augment the operational semantics of an idealized assembly language with additional rules that model erroneous control-flow transfers. Next, we explain a strategy for detecting control-flow errors based on previous work by Oh [10] and Reis [15]. In order to reason about the correctness of the strategy relative to our fault model, we develop a new assembly-level type system designed to guarantee that any control flow transfer to an incorrect block will be caught before control leaves that block. The key technical result of the paper is a rigorous proof of this fundamental control-flow property for well-typed programs.
UR - http://www.scopus.com/inward/record.url?scp=49049102729&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=49049102729&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-69166-2_22
DO - 10.1007/978-3-540-69166-2_22
M3 - Conference contribution
AN - SCOPUS:49049102729
SN - 3540691634
SN - 9783540691631
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 332
EP - 346
BT - Static Analysis - 15th International Symposium, SAS 2008, Proceedings
T2 - 15th International Static Analysis Symposium, SAS 2008
Y2 - 16 July 2008 through 18 July 2008
ER -