Flow-sensitive type qualifiers

By Jeffrey S. Foster, Tachio Terauchi, A. Aiken. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2002

381 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems, Software

View Paper: https://www.semanticscholar.org/paper/39ca005f6e0c9c28155082640d7eaa52e5148986

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Software

Citations in the corpus

Dependent types for JavaScript (2011, methodology): “We use an SMT solver to reason about the properties it tracks well, namely, control-.ow invariants and dictionaries with dynamic keys that bind scalar values.”
Software model checking (2009, positive): “Examples of such analyses include type qualifiers [Foster et al. 2002] and typestate interpretations [Fahndrich and DeLine 2004], which map from typestates to predicates over an object’s fields, which can be exploited to verify object-oriented programs using inheritance.”
Abstractions from proofs (2004, background): “These two features are often mutually exclusive: flow based interprocedural analyses [11, 15] achieve scalability by fixing a small domain of dataflow facts to be tracked, and compute flow functions over the abstract semantics of the program on this fixed set.”
Lazy abstraction (2002, background): “In most cases, correctness cannot be proven using a dataindependent analysis [19], and requires the automatic discovery of relevant predicates.”
Sound and precise analysis of web applications for injection vulnerabilities (2007, methodology): “They used a CQual-like [ 5 ] type system to propagate taint information through PHP programs.”
SMART: Secure and Minimal Architecture for (Establishing a Dynamic) Root of Trust (2012, methodology): “Properties (1) and (2) are guaranteed by using two code instrumentation tools: CQUAL [19] and Deputy [11].”
Static detection of cross-site scripting vulnerabilities (2008, methodology): “They used a CQual-like [4, 5] type system to propagate taint information through PHP programs.”
SMART: Secure and Minimal Architecture for (Establishing Dynamic) Root of Trust (2012, methodology): “CQUAL propagates this type to each variable that is computed with any involvement of any other variable of type SECRET.”
ESP: path-sensitive program verification in polynomial time (2002, methodology): “The flow-sensitive type qualifier system [19] is similar to the analysis engine in ESP, but is less precise, because it does not handle branch correlation, and it is not contextsensitive with respect to the property state.”
Static Detection of Security Vulnerabilities in Scripting Languages (2006, methodology): “Other tainting analysis that are proven effective on C code include CQual [ 4 ], MECA [21], and MC [6, 2]. Collectively they have found hundreds of previously unknown security errors in the Linux kernel.”
Finding bugs is easy (2004, methodology): “The authors have used CQual to find format string vulnerabilities [43] and locking bugs [ 26 ].”
Securing web application code by static analysis and runtime protection (2004, background): “[28] extended their original, flow-insensitive type qualifier system for C with flow-sensitive type qualifiers.”
A system and language for building system-specific, static analyses (2002, positive): “Cqual [14] is an annotation-based approach that adds flow-sensitive qualifiers to standard C types.”