SYSGO organized this workshop which was co-located with the Embedded Software Engineering Kongress 2019. This year's edition had 25-30 registered attendants. Good and productive discussions were held on the different design and verification approaches presented and on their relation to MILS.

Here is a short summary of the talks held at the MILS Workshop 2019:

Sergey Tverdyshev from SYSGO spoke on high-level concept architectural approach of MILS, whose first concepts go back to more than 40 years. News since last MILS workshop included ongoing work at Common Criteria Users' Forum together with the virtualization working group and that two separation kernels obtained Common Criteria certifications. Moreover, in the certMILS project, a partitioned design received one of the first IECEE IEC 62443-4-1 certifications ever. While in the CITADEL project, work on adaptive MILS has been done, including demonstrations in voice processing and subway environments.

Pierre Girard from Gemalto used the challenge of securing cars as a motivational example, taken from his work. Pierre then gave an overview of the different options to create assurance via deploying security primitives such as e.g. keys as distributed system, ranging from process isolation, via dedicated coprocessors, dedicated cores to dedicated chips. He gave an example where the PikeOS MILS separation kernel used keys stored in a dedicated secure environment.

Daniel Schreckling from BMW gave an example of security monitors in an E/E architecture. In a typical safety critical system there is not necessarily a central entity and he suggested that the data layer itself provides its security policies and reference monitors in a decentral way. The information flows and security policies implied by the local reference monitors can be checked via offline static model checking and/or online dynamic model checking. The kind of information flow monitoring and / or control needed could be provided by dedicated hardware and / or MILS systems.

Juan Sanchez from DEKRA works in security testing. He reported on his experiences of IEC 62443 and Common Criteria penetration testing. He mentioned, based on examples, typical vulnerabilities that he was able to exploit. For instance, in a blackbox testing of a communication dongle he was able to extract data such as a vehicle identification numbers from unencrypted bluetooth, access lightning control via OBD-II and upload of malicious files to the customer servers. We discussed that MILS security by design is currently not yet implemented in many devices Juan gets on the table today, but that this might change when higher assurance is needed.

Finally, Daniele Lacamera from wolfSSL showed small footprint implementations of cryptographic implementations, which are e.g. widely used in automotive embedded systems. Certification activity includes FIPS. Licensing is dual-licensing i.e. commercial and open source GPLv2 license. MILS separation kernels are often used to protect the cryptographic keys and operations of these cryptographic algorithms e.g. in mixed criticality systems.