interfering

Tech stack & purpose

The "interfering" project is a Coq formalization of research on machine security properties, specifically formalizing concepts from an academic paper on stack integrity and confidentiality. The development is built in Coq and maps formal structures including machine states, policies, traces, and observations to corresponding definitions in files such as Machine.v, ObsTrace.v, and formal.v. The formalization includes multiple security properties—such as eager and lazy stack integrity, stack confidentiality, and well-bracketed control flow—along with theorems proving these properties hold under various execution models.

Languages

Contributors

• Sean405 commits
• Andrew Tolmach367 commits
• 
  Rob Blanco348 commits · 0 followers
• Sean Anderson313 commits
• 
  Benjamin Pierce277 commits · 319 followers
• Leonidas Lampropoulos238 commits
• lemonidas2 commits