Topic: type-safe and secure languages

topics > computer science > data > Group: type checking

program proving
types of programming languages

compiler error checking
consistency testing
error safe systems
flavor analysis and typestates for supplementary type checking
mobile code
model checker
operating system security
preventing accidental errors
proof-carrying code
run-time assertions
safety critical systems
safety, liveness, and system properties
security of remotely executed code
weak vs. strong type checking

Subtopic: formal semantics up

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 up

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 up

Quote: type checking ensures well-defined operations on data; security checking ensures authorization to execute operations [»brinP_1973]

Subtopic: type safety up

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 up

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 up

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 up

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 up

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 up

Quote: use typeflow analysis to detect errors and reduce dynamic type testing of Oberon-style types [»cornD3_1994]

Subtopic: synchronous language up

Quote: use synchronous languages for real-time, embedded, safety critical applications [»benvA1_2003]

Subtopic: validated input up

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 up

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 up

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 up

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 up

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 up

Quote: Microsoft gave up on security by adding C and C++ to the CLR; unsafe regions in C# allow unrestricted pointer operations

Related Topics up

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)

Updated barberCB 10/06
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.