search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

Secure #218

Closed lag47 closed 2 years ago

lag47 commented 2 years ago

The final of three pull requests intended to bring the secure branch into master. This pull request contains all of the code included in the trace and dijkstra_pull_request branches, but it focuses on a mechanization of two information flow indistinguishability relations over ITrees, eqit_secure and pi_eqit_secure. The former formalizes progress sensitive indistinguishability and the latter formalizes progress insensitive indistinguishability.

This pull request also formalizes a bunch of meta theory about these relations, for instance progress sensitive indistinguishability lifts PERs over return types to PER's over ITrees. It also includes two verified information flow type systems for Imp (with print + exceptions) and a proof that a compiler from Imp to Asm preserves noninterference.

Lysxia commented 2 years ago

To avoid accidentally adding .DS_Store files in the future, you can put a .gitignore file in your home directory and it will apply to everything on your machine.

Lysxia commented 2 years ago

These additions seem big enough to warrant releasing them as a new package. We can still keep everything in the same repository.