Safety and Security UndeR Focal – SSURF

The proposed project consists both :
- in characterizing and studying the required features that an Integrated Development Environment (IDE)
must provide in order not only to obtain sofware systems in conformance with high Evaluation Assurance
Levels (EAL-5 6 7), but also to ease the evaluation process according to standards (IEC61508, CC, ...),
and
- in developping a formal generic framework describing various security properties such those of access
control policies together with their implementations using such an IDE.
These two parts are strongly connected, the second part playing the role of a true running example for
the first one while requiring for new theoretical results/extensions/tools from the first part. They are
both concerned with methological aspects, semantics, logics, proof systems, compilation, rewriting, and
computer science security. However, while the first part aims to elaborate features for an IDE of general
purpose, the second one aims to provide a theoretical framework in which security properties such as
access control policies and their implementations can be specified, defined, compared and proved. This
theoretical framework will be implemented within the considered IDE, providing a non-trivial illustration
of its use.
This work will be based on the Focal environment which already provides tools to write specifications,
programs, properties and proofs at the same level, proofs being ultimately checked by Coq and programs
compiled to Ocaml.