Team for Research in
Ubiquitous Secure Technology

Citation
J. Foster, J. Kodumal, R. Johnson, A. Aiken. "Flow-Insensitive Type Qualifiers". ACM Transactions on Programming Languages and Systems, 2006.

Abstract
We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming languages with static type systems, such as C and Java. In our system, programmers add a few type qualifier annotations to their program, and automatic type qualifier inference determines the remaining qualifiers and checks the annotations for consistency. We describe a tool CQual for adding type qualifiers to the C programming language. Our tool CQual includes a visualization component for displaying browsable inference results to the programmer. Finally, we present several experiments using our tool, including inferring const qualifiers, finding security vulnerabilities in several popular C programs, and checking initialization data usage in the Linux kernel. Our results suggest that inference and visualization make type qualifiers lightweight, that type qualifier inference scales to large programs, and that type qualifiers are applicable to a wide variety of problems

Electronic downloads

• http://theory.stanford.edu/~aiken/publications/papers/toplastq.pdf

• HTML

  J. Foster, J. Kodumal, R. Johnson, A. Aiken. <a
  href="http://www.truststc.org/pubs/610.html"
  >Flow-Insensitive Type Qualifiers</a>, <i>ACM
  Transactions on Programming Languages and Systems</i>,
   2006.

• Plain text

  J. Foster, J. Kodumal, R. Johnson, A. Aiken.
  "Flow-Insensitive Type Qualifiers". <i>ACM
  Transactions on Programming Languages and Systems</i>,
   2006.

• BibTeX

  @article{FosterKodumalJohnsonAiken06_FlowInsensitiveTypeQualifiers,
      author = {J. Foster and J. Kodumal and R. Johnson and A.
                Aiken},
      title = {Flow-Insensitive Type Qualifiers},
      journal = {ACM Transactions on Programming Languages and
                Systems},
      year = {2006},
      abstract = {We describe flow-insensitive type qualifiers, a
                lightweight, practical mechanism for specifying
                and checking properties not captured by
                traditional type systems. We present a framework
                for adding new, user-specified type qualifiers to
                programming languages with static type systems,
                such as C and Java. In our system, programmers add
                a few type qualifier annotations to their program,
                and automatic type qualifier inference determines
                the remaining qualifiers and checks the
                annotations for consistency. We describe a tool
                CQual for adding type qualifiers to the C
                programming language. Our tool CQual includes a
                visualization component for displaying browsable
                inference results to the programmer. Finally, we
                present several experiments using our tool,
                including inferring const qualifiers, finding
                security vulnerabilities in several popular C
                programs, and checking initialization data usage
                in the Linux kernel. Our results suggest that
                inference and visualization make type qualifiers
                lightweight, that type qualifier inference scales
                to large programs, and that type qualifiers are
                applicable to a wide variety of problems},
      URL = {http://www.truststc.org/pubs/610.html}
  }
  

Posted by Jessica Gamble on 17 Mar 2009.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.