Programming language-based security is realized by primitive features and mechanisms for specifying and enforcing security policies in languages, providing a foundation for secure software development. Java has paved the way for popular acceptance of this approach: the combination of stack inspection, namespace management, and bytecode verification in the JVM allows specification and rigorous enforcement of practical policies such as sandboxing.
Some language-based security features are enforced at run-time, but a distinct benefit of the language-based approach is that it allows compile-time, aka static, enforcement of security policies expressed via linguistic primitives. In particular, we have shown how type theories can be used for the static enforcement of Java stack inspection, and also for enforcement of capability-based security. Static enforcement of these security models allows earlier detection of security violations, eliminating the need for costly run-time checks, and in some cases allowing compiler optimizations otherwise precluded by run-time security semantics. Type theories provide precision and flexibility, via e.g. parametric polymorphism and subtyping constraints, as well as a rigorous mathematical foundation for formal guarantees of security.
This is joint work with Scott Smith and François Pottier.
Trace effects are a form of type-and-effect that statically approximate run-time event traces, where events are records of some program action (similar to log entries). A principal novelty of trace effects is that they express temporal ordering of events. We have established a foundational theory of trace effects, which shows how artifacts of type reconstruction can be combined with model checking techniques to provide a powerful program logic based on temporal logic assertions. Type theoretic technology also promotes scalability, and we have also shown that trace effects apply to object-oriented languages such as Java and other advanced language features.
Flow effects are similar to trace effects, but events in the flow effect model are dataflow constraints; for example, if a function f is applied to 5, then an event recording the flow of an integer type into the domain type of f is recorded. Because flow effects also account for temporal ordering, the analysis is context sensitive.
This is joint work with Scott Smith, Paritosh Shroff, and David Van Horn.
This work is supported by a DoD DEPSCoR grant through the Air Force Office of Scientific Research.
Trust management systems provide a framework for authorization of non-local users of some resource over a network. Examples include KeyNote, SDSI/SPKI, and RT. Authorization decisions in these frameworks are often viewed as proofs of propositions involving the requestor and the resource, where certificates function as axioms. However, if proofs are complex, ideal security may need to be simplified for the sake of practical online authorization; nevertheless, it is desirable to be able to verify these simplifications offline, as a matter of course or if the need arises. We have recently developed a trust but verify (TbV) approach to trust management, where simplified online authorization decisions are required to have a formal relation with "ideal" authorization specifications, so that offline checking can be guaranteed to verify ideal security.
In a similar vein, we have extended the RT framework with an additive notion of risk, yielding the language RTR. Risk is defined in an abstract manner, and can be wait-times, age of certificates, trustworthiness of the issuer, etc. We also define a certificate chain discovery algorithm that is directed, in the sense that it never attempts to retrieve certificate chains that overrun a given risk threshold.
On a more foundational level, we have been investigating the use of the LolliMon linear logic programming language for the specification and implementation of the RT framework. This solution is more scalable and easily verifiable than graph-theoretic approaches, and more applicable to certificate chain discovery problems than Datalog or Prolog.
This is joint work with Jeff Polakow, X. Sean Wang and Peter Chapin.