SpAGAT
Secrecy and Information Flow in Shared Document Bases
The subject of this project is the analysis of secrecy and information flow in applications
where multiple users execute a workflow while sharing a common document base. Our
objective is to generalize classic notions of secrecy such as noninterference so that the
designer can precisely state the intended information flow as it changes over time in
response to changes in the state of the workflow as well as strategic choices by the different
users of the system. The new specification language will be supported by a semantically
substantiated security analysis based on a multi-player game model of the interaction
between the users. Extending counterexample-guided abstraction refinement (CEGAR)
to such models, we will obtain automatic methods for verification and certificate synthesis.
Principal Investigators
|
Projects