Safety/Security Policies

"Enforceable security policies" characterizes the class of security policies enforceable by execution monitors. In this paper, security policies in general is specified by giving a predicate on sets of executions. It is classified into properties and non-properties. A property can be specified as a predicate on individual executions. The information flow property is not a property because it depends on sets of executions instead of individual executions. A property can be classified into safety properties, liveness properties, and safety+liveness properties. A safety property stipulates that no "bad thing" happens during any execution. Execution monitors can only enforce safety properties.

"Computability classes for enforcement mechanisms" discusses the computability classes for various enforcement mechanisms: static analysis, execution monitoring, and program rewriting. Security policies enforceable by static analysis (including type systems) is the class of recursively decidable properties of programs. The set of security policies enforceable by program rewriting is a superset of the set of security policies enforceable by execution monitoring, since execution monitoring needs to explicitly stop whenever the policy is violated, while program rewriting does not need to stop.

"A language-based approach to security" promotes a language-based approach to security: Better performance cost than hardware protection; More flexible; Moderate TCB.

"Type systems" classifies execution errors into trapped errors and untrapped errors. Type systems should rule out all untrapped errors and some trapped errors (called forbidden errors together). Cardelli defines type safety to be the property stating that programs do not cause untrapped errors; type soundness to be the property stating that programs do not cause forbidden errors. Then the paper presents many type systems: first-order type systems; second-order type systems; with product types, union types, record types (labelled product), variant types (labelled union), reference types, and recursive types; with subtyping.

Logical Frameworks/Twelf

"Logical Frameworks--A Brief Introduction" by Frank Pfenning presents an excellent introduction to LF methodology: How to represent syntax and deductions of object logic in LF meta-logic; Higher-order representations; The "judgment-as-types" principle; The adequacy of representations.

"A Framework for Defining Logics" by Harper, Honsell and Plotkin presents a technical account of LF. It presents the syntax and typing rules of LF, which is dependently-typed lambda calculus. As examples, the paper presents adequate encodings of First-Order Logic and Higher-Order Logic (both syntax and deductions). On the theoretical aspect, the paper proved that type checking in LF is decidable, which makes it possible to build tools such as Twelf. LF is decidable simply because its terms are similar to those in simply-typed lambda calculus, and satisfy strong normalization and Church-Rosser Property.

"Higher-Order Abstract Syntax" by Pfenning and Elliott proposed the use of HOAS as a central representation for programs, formulas, rules, and other syntactic objects in formal systems. The idea is to use variables in a meta logic (such as LF) to represent variables in the system to represent. Issues such as binding and substitutions can directly leverage the mechanisms in the meta logic. Sec 3.4 presented a technique called raising, which shows that HOAS can finely control the occurrence of free variables.

"A Type-Theoretic Approach to Induction with Higher-Order Encodings" and "Recursion for Higher-Order Encodings" by Schurmann provides an exposition to notions in Twelf such as the regular-world assumption, subordination, and higher-order induction. They have not been explained in the Twelf manual (version 1.4).

Linear Logic

Philip Wadler's "A taste of linear logic" is an excellent tutorial for linear logic. It provides a clear explanation to the differences between AÄB (both A and B), A&B (choose from A and B), and AÅB (either A or B). By separating the context into a linear context and an intuitionistic context, the presentation achieves simple introduction (promotion) and elimination (dereliction) rules for the ! (of course) operator.

"Reference Counting as a Computational Interpretation of Linear Logic" by Chirimar, Gunter and Rieche develops a refrence-counting model for linear logic. An object of type !T is interpreted as a sharable object in memory, while an object of a linear type is interepreted as a linear value in memory. The main goal of the paper is to formalize the intuitive invariant in linear logic that "linear values have only one pointer to them". The paper shows the invariant has to be stated with careful assumptions. The paper also develops interestings abstractions useful for reasoning about memory: memory graphs, the root set, the reference count of a location.

Last updated: 12/30/2005

Author : Gang Tan, Boston College. Send comments to gtan AT