Reasoning about control flow in the presence of transient faults

Frances Perry, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages332-346
Number of pages15
DOIs
StatePublished - 2008
Event15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain
Duration: Jul 16 2008Jul 18 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5079 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th International Static Analysis Symposium, SAS 2008
Country/TerritorySpain
CityValencia
Period7/16/087/18/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Reasoning about control flow in the presence of transient faults'. Together they form a unique fingerprint.

Cite this