Group:
program proving
Group:
security
Topic:
code optimization
Topic:
code optimization by flow analysis
Topic:
consistency testing
Topic:
debugging by usage rules
Topic:
dependency analysis
Topic:
immutable files and data
Topic:
model checker
Topic:
optimization of object-oriented programs
Topic:
preventing accidental errors
Topic:
race conditions
Topic:
run-time assertions
Topic:
safe use of pointers
Topic:
safety, liveness, and system properties
Topic:
static single assignment; SSA
Topic:
type-safe and secure languages
Topic:
weak vs. strong type checking
| |
Summary
Typestate is a type annotation developed by Strom and Yemini for capturing initialization information. Typestate checking prevents errors due to uninitialized data. For example, if data is set in one branch, but not in another, typestate will catch this. They found this increased the locality of errors.
Winner proposed an 'unassigned' value as a generalization of NIL to explicitly make a variable dead. (cbb 1/90)
Subtopic: typestate -- type annotation 
| Quote: a typestate is a type annotation that captures state attributes such as uninitialized; mutually exclusive [»stroRE1_1986]
| | Quote: with typestate checking can not initialize an object in only one branch of a conditional [»stroRE1_1986]
| | Quote: typestate captures the degree of initialization of simple and composite objects [»stroRE5_1985]
| | Quote: typestate information forms a lower semilattice
| | Quote: an operation in NIL has unique typestate preconditions and unique typestate postconditions for normal and exception exits [»stroRE5_1985]
| | Quote: when multiple control paths join, typestate is greatest lower bound of incoming typestates [»stroRE5_1985]
| | Quote: algorithm for checking typestate consistency, e.g., initialization [»stroRE1_1986]
| | Quote: in NIL, module definitions include typestate transitions for parameters; allowed independent development [»stroRE5_1985]
| | Quote: NIL's typestate interfaces meant that system testing did not reveal new errors in unit-testing; locality of errors was assured [»stroRE5_1985]
| | Quote: safety check of untrusted machine code by typestate analysis; allows manipulation of host data structures; checks array bounds, address alignment, initialization, null pointers, stack manipulation [»xuZ6_2000]
| | Quote: safety check recursive programs by using the induction-iteration method to synthesize invariant entry conditions; not implemented [»xuZ6_2000]
| | Quote: Vault as a safe C with execution-ordering constraints; object in one of several states; annotate functions for their effect on object state [»laruJR5_2004]
| | Quote: Vault identifies non-aliasing objects for type state analysis
|
Subtopic: design specification
| Quote: explicit specification of a procedure's design information documents the programmer's intent, allows compile-time checking, provides modularity, and enables lexical analysis and separate compilation [»rugiR4_2001]
| | Quote: pointer interfaces specify how procedures change the points-to information [»rugiR4_2001]
| | Quote: region interfaces specify the regions of memory accessed by a procedure
| | Quote: defining pointer and region interfaces simplified the automatic parallelization of Quicksort and other algorithms [»rugiR4_2001]
|
Subtopic: counterexamples & open programs
| Quote: Chord analyzes open programs and reports counterexamples; essential; detect races before deployment [»naikM6_2006]
| | Quote: report counterexamples for each race, categorized by field and by object; which threads, which objects, and which locks [»naikM6_2006]
|
Subtopic: flavor analysis -- data properties
| Quote: flavor analysis: check assumptions about data properties from assertions of those properties along all flows of control [»howdWE12_1989]
| | Quote: a flavor is a property of an object that changes during program execution; e.g., 'total' may be initialized, partial sum, total sum [»howdWE1_1990]
| | Quote: a data state expression in flavor analysis is the set of data properties that objects can have at a program location
| | Quote: use assumption and assertion comments to state that x has a single property or some property with other properties [»howdWE1_1990]
| | Quote: flavor and scheduling analysis by comment analysis on data state and operator state expressions; give assumptions and assertions [»howdWE1_1990]
| | Quote: input flavor statements specify data assumptions at function invocation; output statements specify data assertions at end [»howdWE1_1990]
| | Quote: a data state expression in flavor analysis is the set of data properties that objects can have at a program location
| | Quote: operator state expressions--an assumption denotes the programmer's expectation that all paths imply some operator state; an assertion becomes part of the operator state [»howdWE1_1990]
| | Quote: an operator state expression in scheduling analysis is the valid operator sequences that can reach a program location
| | Quote: an always flavor statement specifies data assumptions at every program location
| | Quote: the flavor analyzer does not interpret data objects; so A(T) and A(R) are treated separately [»howdWE1_1990]
| | Quote: flavor analysis treats task invocation and return the same as subroutine invocation and return [»howdWE1_1990]
| | Quote: handle infeasible paths by assigning flavors to a special 'path condition'; stop path exploration when the flavor assumption fails [»howdWE1_1990]
| | Quote: flavor analysis enormously useful for checking assumptions about temporaries and registers; particularly for maintenance [»howdWE12_1989]
| | Quote: used flavor analysis on an existing 70K assembly language program; effective for tracking registers and temporary variables [»howdWE1_1990]
|
Subtopic: path analysis
| Quote: PREfix for path-by-path analysis across function boundaries; finds null pointers, improper memory allocation/deallocation; uninitialized variables, resource state errors, improper library usage [»laruJR5_2004]
|
Subtopic: pointer analysis
| Quote: CCured identifies safe pointers, sequence pointers that require bounds check, and wild pointers that require a type checks [»necuGC5_2005]
| | Quote: CCured identifies forward sequence pointers and other pointer kinds [»necuGC5_2005]
|
Subtopic: type guard, proper usage
| Quote: Vault defines type guards for specifying resource management protocols; e.g., operations performed in a valid order, operations required before access, operations that will be performed; enforced at compile time [»deliR6_2001]
| | Quote: a type specifies the valid operations while a type guard specifies when an operation is valid
| | Quote: a type guard consists of a key and optional local state; the key must be in the global held-key state when accessing the variable [»deliR6_2001]
| | Quote: Vault's type system is based on Capability Calculus and alias types [»deliR6_2001]
|
Subtopic: annotation
| Quote: fix security warnings or add annotations; run Splint until done [»evanD1_2002]
| | Quote: annotations and static analysis identified format bugs, buffer overflow bugs, and unknown flaws in wu-ftpd [»evanD1_2002]
| | Quote: use annotations for static analysis of properties such as not-null or unique-reference [»evanD1_2002]
| | Quote: use 'confine' and 'restrict' to track lock state; removed spurious type errors in 138 of 152 device driver modules [»aikeA6_2003]
| | Quote: read-only should be the default type annotation [»tschMS10_2005]
|
Subtopic: field property
| Quote: field properties refine type information for reference fields; e.g., does not reference subclasses of C, contains fixed-size array [»ghemS6_2000]
| | Quote: implement field analysis with static, single-assignment (SSA) graph; analyze loads and stores without optimization or context-sensitive information [»ghemS6_2000]
| | Quote: field analysis in linear time by code size; 10% cost; 7% faster
| | Quote: a field inherits its assignability and mutability from the field's references; mutability is transitive by default [»tschMS10_2005]
| | Quote: Javari guarantees that a read-only reference cannot be used to reassign any field in the object's protected, abstract state [»tschMS10_2005]
|
Subtopic: memory region annotation
| Quote: use annotations to track memory regions across function calls
| | Quote: avoid memory errors by partitioning memory into pools according to the points-to graph; allows aggressive interprocedural pointer analysis; only 10% overhead due to static checking [»dhurD6_2006]
| | Quote: detect invalid references by partitioning memory according to its points-to graph; homogeneous pools avoid dangling pointers and run-time checks [»dhurD6_2006]
|
Subtopic: annotation for race detection
| Quote: type annotation for static race detection; found errors in Java libraries; 20 annotations per 1000 lines [»flanC6_2000]
| | Quote: type annotations--'guarded_by lock' for fields and 'requires lock_list' for methods; 1000 lines per programmer hour [»flanC6_2000]
| | Quote: use Flanagan and Abadi's race-free type system to prove that Guava objects are never concurrently accessed [»bacoDF10_2000]
| | Quote: Chord uses annotations to specify which threads can not execute in parallel; 42 annotations per 1.5 million lines of code [»naikM6_2006]
|
Subtopic: unassigned, uninitialized
| Quote: can have a value 'unassigned' that makes a variable uninitialized [»winnRI10_1984]
| | Quote: run-time checks of actual types; unallocated, uninitialized, integral, real, and pointer; shows exact location of errors; 20x slower [»logiA4_2001]
|
Subtopic: array bounds
| Quote: efficient array bound checking across procedure calls; reports name and dimension of erroneous array; uses source-to-source Fortran compiler and convex array regions [»nguyTV5_2005]
| | Quote: symbolic bounds analysis for static race detection, automatic parallelization, array bounds analysis, size of computed values; determines upper and lower bounds for array indices and pointers [»rugiR3_2005]
|
Subtopic: mirror of memory
| Quote: store run-time type information in a mirror of memory, 4 bits/byte; continuation bit, type, and size; two nibbles identifies an object [»logiA4_2001]
|
Subtopic: examples
| Quote: CSSV for static analysis of buffer overflows in C; optional contract per procedure reduces to integer expressions; handles heap allocation, multi-level arrays, function pointers, casting; faster than authors' previous algorithm [»dorN6_2003]
|
Subtopic: limitations of type analysis
| Quote: avoid using annotations to guide the constraint solver; error-prone [»zandBT11_2005]
| | Quote: use static analysis, symbolic interpretation, reachability, and logic model checking for non-deterministic software; but bugs will still remain
| | Quote: limitations of safety check -- does not work for local arrays, multiple array-typed fields, array references, subclasses, non-linear constraints [»xuZ6_2000]
| | Quote: induction-iteration for typestate, safety checking can not detect array errors if correctness depends on values outside of the loop
|
Related Topics
Group: program proving (10 topics, 311 quotes)
Group: security (23 topics, 874 quotes)
Topic: code optimization (54 items)
Topic: code optimization by flow analysis (47 items)
Topic: consistency testing (60 items)
Topic: debugging by usage rules (41 items)
Topic: dependency analysis (34 items)
Topic: immutable files and data (59 items)
Topic: model checker (49 items)
Topic: optimization of object-oriented programs (16 items)
Topic: preventing accidental errors (37 items)
Topic: race conditions (33 items)
Topic: run-time assertions (25 items)
Topic: safe use of pointers (102 items)
Topic: safety, liveness, and system properties (22 items)
Topic: static single assignment; SSA (19 items)
Topic: type-safe and secure languages (43 items)
Topic: weak vs. strong type checking
(42 items)
|
