[UVM logo]

Christian Skalka, Research Project Details

Home | Research Interests | Research Projects | Teaching | Publications | Presentations

Static Language-Based Access Control

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.

Valid XHTML Valid CSS