Effective blame for information-flow violations

Dave King, Trent Jaeger, Somesh Jha, Sanjit A. Seshia

Abstract

Programs trusted with secure information should not release that information in ways contrary to system policy. However, when a program contains an illegal flow of information, current information-flow reporting techniques are inadequate for determining the cause of the error. Reasoning about information-flow errors can be difficult, as the flows involved can be quite subtle. We present a general model for information-flow blame that can explain the source of such security errors in code. This model is implemented by changing the information-flow verification procedure to: (1) generate supplementary information to reveal otherwise hidden program dependencies; (2) modify the constraint solver to construct a blame dependency graph; and (3) develop an explanation procedure that returns a complete and minimal error report. Our experiments show that information-flow errors can generally be explained and resolved by viewing only a small fraction of the total code.

BibTeX

@inproceedings{King-al:FSE08,
  author    = {Dave King and
               Trent Jaeger and
               Somesh Jha and
               Sanjit A. Seshia},
  title     = {Effective blame for information-flow violations},
  booktitle = {FSE},
  pages     = {250--260},
  publisher = {{ACM}},
  year      = {2008},
}

Effective blame for information-flow violations

Abstract

Related papers