Security Type Error Diagnosis for Functional Languages
Date: Wed, May 22, 2019
Room: Lecture Hall L (building 36)
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.
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