Group:
program proving
Group:
security
Group:
types of programming languages
Topic:
compiler error checking
Topic:
consistency testing
Topic:
error safe systems
Topic:
flavor analysis and typestates for supplementary type checking
Topic:
mobile code
Topic:
model checker
Topic:
operating system security
Topic:
preventing accidental errors
Topic:
proof-carrying code
Topic:
run-time assertions
Topic:
safety critical systems
Topic:
safety, liveness, and system properties
Topic:
security of remotely executed code
Topic:
weak vs. strong type checking
| |
Subtopic: formal semantics 
| Quote: without a formal semantics or a formal type system, can not reason about Java or the security properties of its libraries [»deanD5_1996]
|
Subtopic: secure language
| Quote: a programming language is secure if it does not lead to machine or implementation effects that are inexplicable in terms of the language [»hoarCA_1974]
| | Quote: a language is secure if it detects most cases where its concepts break down and produce meaningless results [»brinP4_1999]
| | Quote: correct if correct input leads to correct output; secure if arbitrary inputs do not have undesired consequences [»mitcJC1_2001]
| | Quote: with Java, new code starts untrusted, becomes verified, then transformed into machine code by a trusted compiler [»allmE7_2004]
| | Quote: type checking authenticates valid types prior to processing and keeps secret the procedures that implement the type [»morrJH10_1973]
|
Subtopic: security checking
| Quote: type checking ensures well-defined operations on data; security checking ensures authorization to execute operations [»brinP_1973]
|
Subtopic: type safety
| Quote: in Modula-3 every expression has a unique type with a simple subtype relation [»nelsG_1991]
| | Quote: Modula-3 does not use ambiguous types, target-typing, or automatic conversions (except for packed fields, etc.)
| | Quote: proof of type soundness for a large, sequential sublanguage of Java; via the interactive theorem prover Isabelle/HOL [»nipkT1_1998]
|
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]
|
Subtopic: memory safety
| Quote: compositional verification of memory safety in optimized code; encode low-level safety information via static single-assignment (SSA) proof variables [»menoVS1_2006]
|
Subtopic: safe programs
| Quote: safe programs can share the same address space; no accidental side effects from other programs
| | Quote: an error in a safe program can only cause a run-time error, a wrong answer, or an infinite loop
|
Subtopic: safe vs. unsafe module
| Quote: a safe module includes no unsafe interfaces or operations such as unchecked type transfer, address arithmetic, dispose object, and untraced allocations [»cardL_1991]
| | Quote: a language feature is unsafe if its misuse can corrupt the runtime system; e.g., array assignment without bounds checking [»nelsG_1991]
| | 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]
|
Subtopic: typeflow analysis
| Quote: use typeflow analysis to detect errors and reduce dynamic type testing of Oberon-style types [»cornD3_1994]
|
Subtopic: synchronous language
| Quote: use synchronous languages for real-time, embedded, safety critical applications [»benvA1_2003]
|
Subtopic: validated input
| Quote: enforce type system with run-time validation checks on each argument; e.g., all file names belong to the /tmp directory
| | Quote: a validated element must match its type, since validation yields sensible values; consequence of pure named typing [»simeJ1_2003]
|
Subtopic: proof-carrying code
| Quote: translate an ML-like language into typed assembly language (TAL); proof carrying code [»morrG1_1998]
| | Quote: proof-carrying code by computing the safety predicate and a checkable proof; Floyd's verification conditions [»necuGC10_1996]
| | Quote: simple, fast proof-carrying code; guaranteed conformance with a operating system's safety policy; e.g., network packet filters [»necuGC10_1996]
|
Subtopic: typed assembly language
| Quote: use typed assembly language (TAL) for dynamic patches and type safety; prevents crashes and many incorrect actions [»hickM6_2001]
| | Quote: a typed assembly language enforces closures, tuples, and abstract data types without restricting low-level optimizations such as register allocation
| | Quote: low overhead for dynamic updating of TAL code for I/O-intensive applications such as web servers [»hickM6_2001]
|
Subtopic: language examples
| Quote: Cyclone is a safe dialect of C; avoids buffer overflows, format string attacks, and memory management errors; static analysis plus run-time checks and annotations [»jimT6_2002]
| | Quote: the ESP compiler extracts Spin models for checking; can often fully debug with the model checker [»kumaS6_2002]
| | Quote: Java guarantees memory and type safety at runtime and compile time; programs cannot forge pointers, overrun arrays, or apply an operator to the wrong type [»hartPH12_2001]
| | Quote: in NIL, module definitions include typestate transitions for parameters; allowed independent development [»stroRE5_1985]
| | Quote: PL.8 not standardized despite being a fully-checked language; enforcement of language rules cost less than 10% [»auslM6_1982]
| | Quote: PL.8 guarantees that all array and offset references are within bounds; optimizes run-time checks; checking costs 5-10% [»auslM6_1982]
| | Quote: SafeTSA is compact, type-safe mobile code based on static single assignment; safe by construction with referential integrity, type separation, and type check elimination [»ammeW6_2001]
| | Quote: SD3 extends datalog by associating names with authenticated public keys, e.g., T(x,y):-K$E(x,y) holds if E(x,y) and relation E under keyholder of K [»jimT5_2000]
| | Quote: secure DNS resolver in 10 lines of code; easier to understand than BIND's security policy [»jimT5_2000]
| | Quote: SPIN depends only on Modula-3's interfaces, type safety, and automatic memory management; no dangling pointers or array overflow [»bersBN12_1995]
| | Quote: SPIN uses Modula-3 to guarantee that an extension's interface is obeyed; compiler is part of trusted computing base [»grimR2_2001]
| | Quote: extensible systems run core system services and dynamically composed extensions in the same address space using low-latency, type-safe interfaces [»grimR2_2001]
|
Subtopic: analysis 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]
| | Quote: Lucent uses virtual finite-state machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]
| | Quote: fix security warnings or add annotations; run Splint until done [»evanD1_2002]
|
Subtopic: insecure language
Quote: Microsoft gave up on security by adding C and C++ to the CLR; unsafe regions in C# allow unrestricted pointer operations
[»allmE7_2004]
|
Related Topics
Group: program proving (10 topics, 311 quotes)
Group: security (23 topics, 874 quotes)
Group: types of programming languages (29 topics, 611 quotes)
Topic: compiler error checking (16 items)
Topic: consistency testing (60 items)
Topic: error safe systems (76 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: mobile code (14 items)
Topic: model checker (49 items)
Topic: operating system security (18 items)
Topic: preventing accidental errors (37 items)
Topic: proof-carrying code (7 items)
Topic: run-time assertions (25 items)
Topic: safety critical systems (32 items)
Topic: safety, liveness, and system properties (22 items)
Topic: security of remotely executed code (24 items)
Topic: weak vs. strong type checking
(42 items)
|
