| WP07: SW Development support, quality, evaluation and certification |
|
|
|
The aim is to verify and validate the operating system produced in WP04. The production of data (testing and formal analyses results) supporting the future certification is the main task in this phase. A significant and representative part of that code is the target of the analyses of this workpackage. We will also develop an open trusted methodology for Verification and Validation and apply advanced testing, risk analysis and verification techniques to this target.  Overview of workpackage 07 - Click to enlarge This task involves the automated and manual testing of the target with the purpose of checking for security flaws. Coverage and structural testing tools are employed. Testing is always targeted towards the security properties. A formal risk analysis of the target will be performed too, using formal languages and building formal models. Such models are useful input to the formal verification of Linux packages and the CC EAL5 certification as they are required during the CC process and will be refined into a more detailed formal specification. Here we do a formal static analysis of the target using some existing tools used on critical embedded applications. Some research will be done on difficult parts of the static analyser, in the aim of analysing the largest part of the application developed in WP04 and improving the tools. This activity provides the necessary glue and methodology to analyse the target. An open trusted verification methodology that will guide the previous tasks along the V&V process is developed for our specific security purposes. The CC certification at level EAL5 is a very ambitious but necessary goal for every OS maker. The necessary items, documents, processes and tasks to reach CC EAL5 for the OS produced in WP04 are studied in this phase. It will be examined if the code, composed of the combination of a trusted virtualisation layers, either L4 or XEN, and the Linux kernel, is capable of satisfying CC level EAL5 requirements and/or above. |