Publications & Deliverables

Publications

2016

White Paper: Common Criteria Protection Profile (V2.03)[DOI]
Multiple Independent Levels of Security: Operating System
This PP addresses only Operating System as part of a MILS final integrated system. This PP is intended to be part of a set of MILS PPs that should comprise, in the future, also other PPs regarding MILS architecture, like a PP addressing both underlying Hardware Platform and Operating System together and a PP for the entire integrated system.
I. Furgel, V. Saftig, 2016

Supporting MILS on platforms with distributed IO virtualization
Under submission
J. Maebe, N. Penneman, K. De Bosschere, B. De Sutter, 2016.

Monadic Sequence Testing and Explicit Test-Refinements
This paper was submitted to TAP 2016
Presentation of an abstract framework for sequence testing that is implemented in Isabelle/HOL-TestGen. The framework is based on the theory of state-exception monads, explicitly modelled in HOL, and can cope with typed input and output, interleaving executions including abort, and synchronisation.
A. D. Brucker, B. Wolff, 2016.

2015

Conference Paper: Non-Interfering Composed Evaluation [DOI]
In this document, an extension of the concept for the evaluation of a Composed TOE is presented. This approach, namely the Non-Interfering Composed TOE, is based on the traceable property of the non-interference of two certified TOEs.
I. Furgel, V. Saftig, T. Wagner, K. Müller, R. Schwarz, A. Söding-Freiherr von Blomberg, 2015

Security Architecture and Specification Framework for Safe and Secure Industrial Automation
The paper “Security Architecture and Specification Framework for Safe and Secure Industrial Automation” is going to be presented at CRITIS 2015
S. Tverdyshev, H. Blasum, E. Rudina, D. Kulagin, P. Dyakin, S. Moiseev, 2015

FP7 ICT Trust & Security Projects Handbook
The EURO-MILS consortium contributed to the FP7 ICT Trust & Security Projects Handbook in March 2015 (p. 72)

Non-Interfering Composed Evaluation
EUROMILS is pleased to announce that the paper “Non-Interfering Composed Evaluation” is going to be presented at ICCC 2015
T. Wagner, V. Saftig, I. Furgel, K. Müller, R. Schwarz, A. Söding-Freiherr von Blomberg, 2015

White Paper: Used Formal Methods
This document consists of three chapters:

Chapter 1 describes how Isabelle/HOL works and how to use it in a certification process in a sound way.
Chapter 2: Style Guide. It describes how to write Isabelle theories so that they are suitable for collaborative work and human readers in a certification context.
Chapter 3: Compliance statement. We state how, in the EURO-MILS project, the developed theories are compliant with (1) and (2).

H. Blasum, O. Havle, S. Tverdyshev, B. Langenstein, W. Stephan, A. Feliachi, Y. Nemouchi, B. Wolff, C. Proch, F. Verbeek, J. Schmaltz, 2015

Testing the IPC Protocol for a Real-Time Operating System
EUROMILS is pleased to announce that our paper “Testing the IPC Protocol for a Real-Time Operating System” has been accepted at VSTTE 2015
A. D. Brucker, O. Havle, Y. Nemouchi, B. Wolff, 2015

Architecture and Assurance for Secure Systems
Literature (papers and slides) of International Workshop on MILS: Architecture and Assurance for Secure Systems, Amsterdam/The Netherlands, 2015

White Paper: Protection Profile (V1.2)
This Protection Profile addresses only Operating System as part of a MILS final integrated system. In the future there may be also other PPs regarding MILS architecture, like hardware platform or the entire integrated system.
I. Furgel, V. Saftig, 2015

2014

White Paper: MILS Architecture
A generic description of MILS systems and the MILS architecture platform is introduced and the MILS main concepts are discussed. The practical aim is to get a common understanding of MILS terms and definitions, and to provide a framework to derive the information flow, access control and resource allocation of the demonstrators from individual MILS components.
H. Blasum, S. Tverdyshev, B. Langenstein, J. Maebe, B. De Sutter, B. Leconte, B. Triquet, K. Müller, M. Paulitsch, A. Söding- Freiherr von Blomberg, A. Tillequin, 2014

In the proceeding of the Archive of Formal Proofs:
Formal Specification of a Generic Separation Kernel [DOI]
F. Verbeek, S. Tverdyshev, O. Havle, H. Blasum, B. Langenstein, W. Stephan, Y. Nemouchi, A. Feliachi, B. Wolff, J. Schmaltz Archive of Formal Proofs, 2014

In the proceeding of the 33rd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2014), Florence, Italy, September 2014:
On Two Models of Noninterference: Rushby and Greve, Wilding, and Vanfleet
A. Garcia Ramirez, J. Schmaltz, F. Verbeek, B. Langenstein, H. Blasum. Lecture Notes in Computer Science, Springer-Verlag, 2014

In the proceeding of the 10th European Dependable Computing Conference (EDCC 2014), Newcastle upon Tyne, UK, May 2014:
On MILS I/O Sharing Targeting Avionic Systems [DOI]
Kevin Müller (Airbus Group, Munich, Germany), Georg Sigl (Technische Universität München, Germany), Benoit Triquet (Airbus Group, Toulouse, France) and Michael Paulitsch (Airbus Group, Munich, Germany)

2013

Research and Innovation Yearbook 2013
The EURO-MILS consortium contributed to the Research and Innovation Yearbook 2013 (deliverable of the FP7 project “SecCOrd”)

Theorem-Prover Based Test Generation for Circus
A. Feliachi; In Symbolic Methods and Testing, Dagstuhl Reports, Vol 2, Issue 1, p.10, 2013

An Introduction to Model-based Testing with Isabelle/HOL-TestGen
B. Wolff; In Symbolic Methods and Testing, Dagstuhl Reports, Vol 2, Issue 1, p.19, 2013

Decreasing System Availability on an Avionic Multicore Processor Using Directly Assigned PCI Express Devices
K. Mueller, D. Muench, O. Isfort, M. Paulitsch, G. Sigl; In proceedings of EUROSEC 2013; 2013

Test Program Generation for a Microprocessor
A. D. Brucker, A. Feliachi, Y. Nemouchi, B. Wolff; In TAP 2013: Tests And Proofs. Lecture Notes in Computer Science (7942), pages 76-95, Springer-Verlag, 2013

Environment for Specification-based Firewall Conformance Testing
A. D. Brucker, L. Bruegger, B. Wolff; In International Colloquium on Theoretical Aspects of Computing (ICTAC). Lecture Notes in Computer Science (8049), Springer-Verlag, 2013

The Circus Testing Theory Revisited in Isabelle/HOL
A. Feliachi, M.-C. Gaudel, M. Wenzel, B. Wolff; In Formal Methods and Software Engineering. Lecture Notes in Computer Science (8144), pages 131-147, Springer-Verlag, 2013.

Deliverables

Period 3

EURO-MILS Publishable Summary

D21.4 Formal Framework for MILS Integration [DOI]
This document presents our research results about the development of a formal environment to analyse MILS architectures. Its second chapter presents and discusses three existing approaches. This chapter shows their shortcomings. The third chapter proposes possible extensions of Rushby’s model to address them.

D12.3 Common Criteria Protection Profile “Multiple Independent Levels of Security: Operating System” (MILS PP: Operating System) [V2.03, March 2016] [DOI]
The Protection Profile ‘Multiple Independent Levels of Security: Operating System (MILS PP: Operating System)’ addresses only Operating System as part of a MILS final integrated system. The TOE, as addressed in the current Protection, does not include any hardware. If it is desired to certify a TOE also comprising hardware components, the related ST will include these hardware components as part of the TOE.

D13.2 MILS: Business, Legal and Social Acceptance [DOI]
D13.2 is divided into 5 parts: Part I defines the project terminology. Part II presents the results of the business impact analysis of MILS cross-sectorally beyond the avionics and automotive sectors. Part III presents the results of the social impact analysis with a strong focus on consumers. Part IV presents the results of the legal impact analysis of a certified platform with a specific focus on the new paradigm of the Internet of Things and its legal implications and issues. Part V concludes this work.

D21.3 Trustworthy MILS: CC Composite Evaluation Approach [DOI]
As high assurance software systems are becoming more complex and sophisticated, assuring their security and safety is increasingly difficult and costly. Mono-lithic evaluation approaches do not scale well because evaluation effort grows exponentially with the complexity of the evaluation target. To keep pace with growing assurance demands, a compositional evaluation approach is a promising strategy. In a compositional evaluation, the individual components of a system are evaluated independently, and these partial evaluation results are composed to derive the overall evaluation verdict with minimum additional effort. The Common Criteria for IT Security Evaluation (ISO/IEC 15408) and the sup-porting documentation offer two different compositional evaluation schemes: the “Composite Product Evaluation for Smart Cards and Similar Devices” (CPE) and the “Composed Assurance Package” (CAP). In this report, we assess the suitability of CPE in the avionics domain, and we compare this evaluation scheme with its CAP alternative. We use the problem of evaluating an avionic security gateway as a case study to illustrate the implications, advantages, and drawbacks of the CPE approach.

D31.2 Used Formal Methods [DOI]
In this report, the consortium gives arguments why the used formal methods and the model itself are sound. D31.2 consists of three chapters: Chapter 1 describes how Isabelle/HOL works and how to use it in a certification process in a sound way. Chapter 2: Style Guide. Chapter 3: Compliance statement.

D31.4 Test-Generation Methods [DOI]
Methodology, theories, implementation and case-study of a MBT-approach for PikeOS.

D33.1 Addendum to CEM D31.4 Test-Generation Methods [DOI]
This report is a refinement of the CEM (Common Evaluation Methodology) for high assurance. Hence, the aim to this document is to provide additional information to the CEM as a form of suggestion. This information could be used to perform the evaluation of a MILS system or MILS component.

Period 2

EURO-MILS Publishable Summary

Period 1

EURO-MILS Publishable Summary

D12.1 Technical Analysis of Available Assurance Techniques [DOI]
Technical analysis of available assurance techniques proposed by the CC3.1 from EAL 5 to EAL 7 to examine their applicability to a feasible transnational CC certification. Review of known assurance requirements for resource management for existing separation kernels/hypervisors compiled from published protection profiles, security targets or relevant publications.

D21.1 MILS Architecture [DOI]
We give a generic description of MILS systems, our MILS architecture template and discuss MILS main components.

D31.1 Formal specification of a generic MILS seperation kernel D31.4 Test-Generation Methods [DOI]
We introduce a theory of intransitive non-interference for separation kernels with control. We show that it can be instantiated for a simple API consisting of IPC and events.

D41.1 Project website
This deliverable briefly describes the website and its functionality.

D42.1 Project internal and external IT communication infrastructure
This deliverable briefly describes the tools provided within the IT infrastructure to facilitate cooperation and coordination.

D41.2 Initial report on dissemination, standardisation and exploitation
This deliverable reports on the progress of dissemination of the project as well as on standardisation and exploitation of project results during the first EURO-MILS project year. Chapter 1 describes the dissemination approach in EURO-MILS. Chapter 2 covers the standardisation approach and Chapter 3 describes the exploitation approach in EURO-MILS.

April 2016

November 2014

November 2013

June 2013