I. Description of UCL/LVL
The Louvain Verification Lab (LVL) is a research team in the Information and Communication Technologies, Electronics and Applied Mathematics (ICTEAM) institute at Universite catholique de Louvain. It gathers one full-time professor and three PhD students. LVL investigates principles, tools and applications of formal specification, analysis and verification of computer systems, revolving around the automated verification technique known as model checking. The list of publications of the LVL Group is available here.
II. Key persons to the project
Prof. Charles Pecheur is a professor in ICTEAM, UCLouvain. He is interested in formal methods and automated verification, and related aspects of software engineering. He obtained his PhD from Université de Liège. Then he went on a post-doctoral fellowship at INRIA in Grenoble, France, before he crossed the Atlantic to join the Automated Software Engineering Group at NASA Ames in California. He came back to Belgium and Louvain-la-Neuve in 2004.
Dr. Seyed Hossein HAERI is a research fellow on programming languages at UCLouvain with skills in both the theory and practice. Hossein joined SeCloud as an ICTEAM post-doctoral research fellow in Sep 2016. He formerly worked as a post-doctoral research fellow at PLDC (of ICTEAM); as a research assistant at the Hamburg University of Technology, Germany; as an R&D software architect at MuSemantik Ltd., UK; as a research fellow at Heriot-Watt University, UK; and, as an undergraduate research fellow at Sharif University of Technology, Iran.
III. Contributions to the project
UCL/LVL created a model checker that operates on the graphs produced by JIPDA. Model checking is a technique that can statically verify whether a system (in this case the runtime behavior of an application) satisfies certain security properties. For this project, the job of the model checker, therefore, is to statically verify whether security properties expressed through Guardia policies are upheld by an application.
- D2.2.2 describes models and procedures for verifying Guardia security policies through model checking.
- D2.2.4 describes a whole-program model checker for Guardia security policies that works on JIPDA graphs. This deliverable also provides a tool that verifies access control security policies on programs.
D2.2.5 provides a tool that verifies availability.