MECA: an extensible, expressive system and language for statically checking security properties

This paper describes a system and annotation language, MECA, for checking security rules. MECA is expressive and designed for checking real systems. It provides a variety of practical constructs to effectively annotate large bodies of code. For example, it allows programmers to write programmatic annotators that automatically annotate large bodies of source code. As another example, it lets programmers use general predicates to determine if an annotation is applied; we have used this ability to easily handle kernel backdoors and other false-positive inducing constructs. Once code is annotated, MECA propagates annotations aggressively, allowing a single manual annotation to derive many additional annotations (e.g., over one hundred in our experiments) freeing programmers from the heavy manual effort required by most past systems. MECA is effective. Our most thorough case study was a user-pointer checker that used 75 annotations to check thousands of declarations in millions of lines...

• Type: Conference
• Year: 2003
• Where: CCS
• Authors: Junfeng Yang, Ted Kremenek, Yichen Xie, Dawson R. Engler
• Keywords: Annotation, Annotation Language, CCS 2003, MECA Propagates Annotations, Security Privacy