Feedback Oriented Security Analysis
Room: BBL 023
Speaker: Jeroen Weijers
Title: Feedback oriented security analysis
Security analysis can provide a static guarantee that all information flows in a program are secure. We discuss two existing implementations and the feedback they give when an inconsistency is found. A programming language is presented with primitive constructs for protection and declassification. For this language we define the security analysis in a constraint based type and effect system. Our type system is both polymorphic and polyvariant, and has sub-effecting. The set of constraints that were generated by the security analysis are processed by heuristics when an inconsistency is found. We present several heuristics that generate an error message describing the cause of the inconsistency and if possible suggest a fix. We implemented the system and present some error messages that were generated by it.
- 28 Mar 2010