From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: Adrian-Ken Rueegsegger Newsgroups: comp.lang.ada Subject: [ANN] Muen development version 0.6 released Date: Tue, 13 Jan 2015 10:17:54 +0100 Organization: A noiseless patient Spider Message-ID: Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit Injection-Date: Tue, 13 Jan 2015 09:17:26 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="ca501e0e7fcfcc1cfba137a0efd8a6d4"; logging-data="23933"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX196CemJTMX4/yRtHYbESnxe" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.3.0 Cancel-Lock: sha1:D5OlLxbwhXtwgOd3dzmRmpbP6Bk= Xref: news.eternal-september.org comp.lang.ada:24563 Date: 2015-01-13T10:17:54+01:00 List-Id: We are proud to announce the availability of Muen version 0.6, which marks the first official development release. The following major features and improvements have been implemented since the last announcement: * Migration of Muen to SPARK 2014 The kernel code has been migrated from SPARK 2005 to SPARK 2014 [1]. Absence of runtime errors is now verified using the GNATprove tool. Switching to SPARK 2014 enables the use of a larger Ada language subset and contracts are expressed as Ada 2012 aspects. Replacing the SPARK 2005 annotations with Ada 2012 contracts made the code much cleaner. * PCI device passthrough using Intel VT-d (DMAR and IR) Hardware passthrough is realized using Intel's VT-d DMA and interrupt remapping technology. This enables the secure assignment of PCI devices to subjects. * XML policy abstraction and enhanced tool support The XML system description has been modularized and additional abstractions have been added to the policy. This enables users to integrate complex component-based systems running on top of the Muen kernel. Further changes and improvements include: * Support for Intel Haswell architecture * Lightweight subject timer mechanism * Scheduler improvements (minor frame synchronization) * Subject Monitor migrated to SPARK 2014 * Debug server subject Despite the addition of all these new features the kernel has retained its small size. Some numbers regarding the size of Muen: the kernel including the minimal zero-footprint runtime consists of a total of 5308 source lines of code (SPARK/Ada: 4979, Assembly: 329, as reported by SLOCCount version 2.26). A high-level document describing the process of configuring and building a component-based system running on the Muen Separation Kernel is available on the project website [2]. We would also like to mention that we gave a talk about Muen at the High Integrity Software conference HIS 2014 [3] in Bristol. The slides are available online at [4]. Further information is available on the project website [5] and the git repository is at [6]. Please feel free to give the development version of Muen a try. Feedback is much appreciated! Kind regards, Adrian [1] - http://spark-2014.org/ [2] - http://muen.codelabs.ch/muen-toolchain.pdf [3] - http://www.his-2014.co.uk/ [4] - http://www.slideshare.net/AdaCore/slides-his-2014secunethsr [5] - http://muen.codelabs.ch/ [6] - http://git.codelabs.ch/?p=muen.git