Efficient Formally Secure Compilers to a Tagged Architecture General Information

Language: English Existing skills or strong desire to learn: • compilation (for imperative or functional languages); • functional programming (e.g., ML or Haskell); • security, full abstraction, gradual typing; • optional: formal verification in Coq or F? [4]; Context Severe low-level vulnerabilities abound in today’s computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilers, and architectures were designed in an era of scarce hardware resources and too often trade off security for effi-ciency. The semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, estab-lishing security with respect to a high-level semantics does no