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!news.eternal-september.org!.POSTED!not-for-mail From: Adrian-Ken Rueegsegger Newsgroups: comp.lang.ada Subject: [ANN] Muen development version 0.8 released Date: Mon, 6 Feb 2017 19:30:05 +0100 Organization: A noiseless patient Spider Message-ID: Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 7bit Injection-Date: Mon, 6 Feb 2017 18:28:06 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="8f834946c1169c5a0e27fe6ce66b3344"; logging-data="12423"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+FVS7tec5jX7oHFUoLcB62" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Icedove/45.6.0 Cancel-Lock: sha1:buKP70bBIPfliuN7orFgxi+rRkU= Xref: news.eternal-september.org comp.lang.ada:33262 Date: 2017-02-06T19:30:05+01:00 List-Id: -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 We are proud to announce the availability of Muen version 0.8. The following major features and improvements have been implemented since the last release: === Subject Lifecycle With the implementation of a subject loader (SL) component it is now possible to reset and restart subjects at runtime with minimal support from the kernel. The new loader policy abstraction eases the specification of loader subjects which control the lifecycle of one or multiple subjects. Aside from the state, loaders have access to the entire address space of a managed subject in order to be able to set up the execution environment. The new SL component written in SPARK 2014 initializes/resets the writable memory regions of its associated subjects. To find the actual memory regions to process, the loader consults each monitored subject info region by querying it using the new subject info (sinfo) client library. Prior to starting execution of a monitored subject, integrity hashes of each memory region are calculated and compared to their reference value provided by the sinfo data. The demo system has been adapted to make use of this new functionality: the NIC Linux can be restarted by pressing the Right Control+F10 key combination. === System reboot/shutdown The introduction of a new 'kernel' event mode and event actions for system reboot and poweroff enables policy writers to grant subjects the capability to initiate a system reboot or shutdown. If a subject triggers a reboot event, the kernel performs a power-cycle using the Reset Control Register (I/O port 0xcf9). The shutdown functionality is implemented by performing an ACPI shutdown using the poweroff port and the PM1A Control Sleep Type capability. As with the subject restart, the demo system has been extended to showcase the new feature: a system reboot can be triggered by pressing the Right Control+F11 keys while Right Control+F12 initiates a shutdown. === Policy & Toolchain improvements The Muen policy has been extended with a config section which enables the parametrization of a system via the declaration of configuration values. Boolean expressions referencing existing config values can be used to formulate additional properties. The introduction of conditionals that reference config values or expressions selectively enable/disable parts of the policy which allows for flexible customization of a system at integration time. To increase the expressiveness of the policy and ease native component development, component descriptions have been extended with the library construct including dependency declaration. Additionally it is now possible to declare logical devices as well as memory and channel array resources. The new component spec generation tool reads the description of a given component and generates Ada/SPARK packages containing constants of the declared logical component resources. These generated specifications can be used in the component source code to access the declared resources. This ensures a consistent view of the system according to the policy. Physical memory regions can now optionally declare an integrity hash. The SHA-256 hash value can be used to verify the initial content of a given region at runtime. A tool has been implemented that calculates hashes for all physical regions with content (file or pattern). The region hashes are exported as part of the subject info data and used by the SL as described above. === Kernel improvements To prevent potential issues related to Intel Hyper-Threading, e.g. side-channels, the kernel now only activates one thread per physical CPU core. CPUID leaf 11 (Extended Topology Enumeration Leaf) is used to determine the SMT ID of each logical CPU and deactivate it if the ID is non-zero. This effectively disables HT even if no such option is present in the BIOS. Feature-wise, support for event actions has been added. The improved functionality increases the flexibility of the event mechanism and facilitates subject lifecycle management as well as system restart and shutdown. Many other improvements and stabilizations such as e.g. replacement of assembler code with SPARK and reduction of stack size to 4K have been implemented. === Further changes and improvements include * Support for 32-bit Windows VMs using Genode/Virtualbox * Support for Intel Broadwell and Skylake microarchitecture * Support for PCI multi-function device pass-through * Implement tool to statically calculate worst-case stack usage * Implement tool to generate scheduling plans * Implement subject info client library in SPARK 2014 * Update of Linux kernel to version 4.6 * Add support for multiple initramfs per Linux subject With the advent of subject lifecycle management, system shutdown and reboot support and the numerous toolchain improvements, the Muen platform is getting more and more mature. The continuous enhancement and refinement of system policy abstractions, especially the components construct, further simplifies the system specification process and enables the description of complex systems composed of a large number of subjects. We are also thrilled that this release includes the previously announced [1] support for execution of hardware-accelerated 32-bit Windows VMs on top of the Muen SK through the use of Genode/VirtualBox as a deprivileged VMM. A detailed description of the architecture and an account of how this feature came to be can be found in the Genode 16.08 release notes [2]. Last but not least we would like to thank Christiane Kuhn for her contribution of the scheduling plan generation tool [3] which she developed as part of a student project/internship. Further information about Muen is available on the project website [4] and the git repository can be found at [5]. Please feel free to give the latest development version of Muen a try. As always, feedback is very much appreciated! Kind regards, The Muen Team [1] - https://groups.google.com/forum/#!topic/muen-dev/ln7ZrIfDk8c [2] - https://genode.org/documentation/release-notes/16.08#VirtualBox_4_on_top _of_the_Muen_separation_kernel [3] - https://git.codelabs.ch/?p=muen/mugenschedcfg.git [4] - https://muen.codelabs.ch/ [5] - https://git.codelabs.ch/?p=muen.git -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCAAGBQJYmMCtAAoJEMEf4lxkugAyZosP/R0pPd5XgIWKLlN7pIomR4yv mbGk4cP1bBE7KdirdP5Q6FajFCnA+yyP48pfYesiDewXMfLwZqf7CjPIEhtnmfaH kjZYljoUnsZQjak5uvRi426XYWfBTcrnTv7oyfJd2MPkiH7OjYikfG3YVd9L7VFc s1nsqsNh+nw4aifMxp1fhEgIporgACN6rnIlMl/zMLKcYRYguCmqnShhC73ukuj6 yXjLO+gSShVFUr3zzD0/LdUUNNw/PQfXFIotY/lVqt3GP45+VZ49ZFsCGm+es0re DADFSgz3u2M9LHzG089RY4WObKyxrNQdxgb2+v66edmOyGSAtEWZrmI89SgLQFtM w4ETjU4wFtd5mG5JZNYBCWs3JqgrD0g89jH3t+XgpeWzJnF2rTtsSITCApx6DiOg QQKVL/yK5rhEezax6W3wwJ0XCBjfwz8ubZQjURHprrVbWPSbhSpl0pu879iI1Ynn FFvYul9YcxG4FvWjY5y3lpyHVYwRV2NO+MUtQYyURg9Q6lw0EOfHeE/7sQTnQA3Q xBtjQnBzOObbDURecTvKsr/AcHQ5lMEjfv8Isvbu1sT43sfp8c60LYiMeXDuiwDk VXbDK54ZRmCz8zbZUbeOEKW6V2tiCmGWw7rgtNimDCSlqiKwak5z1T8kekP7XtX4 VRxUdN1lO/OGNzzo0fqN =jKON -----END PGP SIGNATURE-----