Security Type Error Diagnosis for Functional Languages

Jurriaan Hage

Security analysis is a validating analysis that verifies that (highly) confidential information in a program does not flow to variables that may also store values of lower confidentiality. If such flows are possible, the program is rejected and a security type error message is provided.

This talk shows how we combine the techniques of type error slicing and type error heuristics to diagnose and explain why a program is not deemed type secure. We have implemented this on top of a type inferencer for a simple functional language extended with security specific language constructs.

---

Previous: Makoto Tatsuta | Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs
Next: Klaus von Gleissenthall (University of California) | Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs