[ANN] Muen development version 0.8 released
159 views
Skip to first unread message
Adrian-Ken Rueegsegger
Feb 6, 2017, 12:20:01 PM2/6/17
to muen...@googlegroups.com
-----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
iQIcBAEBCAAGBQJYmK98AAoJEMEf4lxkugAyhj0QALFt1sIBNGlB2XSKzALLRyPY
ONxpkndAsX1Oy1BThZKbjOVLJ+z7M2U0rDHE27orrdE6XTclL0hjGIbycCyBj9kS
tQodLqbeVVt8YDsVJi74ddtAF+G9rKXcp6BA9B0Mm+1F4ScPGqknsRoFCK96zJv+
GBVnaoedc7c8es9P/H5FEmDAWQBvCsyqZ5GrvNGrdE0BngIaptH5EoszlnqHDS3R
2RiImm85JLN7tGwNfVAXPVJjcvYubplBzEObpB34ngVQnYWUqT8RwLsBo86ewvBh
0mL97NlccArKmpN9cJpCl0Z7/VdUGx/UGZ9VcNUHFtK+w2HwsITKsLbiUX1BnJLS
16D6qL+URgz8eMGPWa8HUp7qOGO7jFF/XnSNPUuHj/h9vREorxfiJNeaN2kAXp3o
Usq60ui2OqD+HzoYw2FtNaXSIzp7bqEVFw+zqKBo5SbeaKDoR97v9+LI1PQugOBN
rza1hIj7lpuJUk1qXCiA8A0fOg6aEDmluP/ijKEw+W01W+jV/g58WwL2vG/XEGPz
tHdQKhDb5FugkcYfRCQLhHBxcNNf2N6catpQJYHithZFzLekSNmhMgwetdYsWOte
gq9fawOqmV+ca2MhM+DuHoypOH8OGR/YpKTQBDsd2Ds7lWGV9a7KtJdcjZh8cEcz
L1O26AeKUHWROucQZBQr
=erbx
-----END PGP SIGNATURE-----
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
iQIcBAEBCAAGBQJYmK98AAoJEMEf4lxkugAyhj0QALFt1sIBNGlB2XSKzALLRyPY
ONxpkndAsX1Oy1BThZKbjOVLJ+z7M2U0rDHE27orrdE6XTclL0hjGIbycCyBj9kS
tQodLqbeVVt8YDsVJi74ddtAF+G9rKXcp6BA9B0Mm+1F4ScPGqknsRoFCK96zJv+
GBVnaoedc7c8es9P/H5FEmDAWQBvCsyqZ5GrvNGrdE0BngIaptH5EoszlnqHDS3R
2RiImm85JLN7tGwNfVAXPVJjcvYubplBzEObpB34ngVQnYWUqT8RwLsBo86ewvBh
0mL97NlccArKmpN9cJpCl0Z7/VdUGx/UGZ9VcNUHFtK+w2HwsITKsLbiUX1BnJLS
16D6qL+URgz8eMGPWa8HUp7qOGO7jFF/XnSNPUuHj/h9vREorxfiJNeaN2kAXp3o
Usq60ui2OqD+HzoYw2FtNaXSIzp7bqEVFw+zqKBo5SbeaKDoR97v9+LI1PQugOBN
rza1hIj7lpuJUk1qXCiA8A0fOg6aEDmluP/ijKEw+W01W+jV/g58WwL2vG/XEGPz
tHdQKhDb5FugkcYfRCQLhHBxcNNf2N6catpQJYHithZFzLekSNmhMgwetdYsWOte
gq9fawOqmV+ca2MhM+DuHoypOH8OGR/YpKTQBDsd2Ds7lWGV9a7KtJdcjZh8cEcz
L1O26AeKUHWROucQZBQr
=erbx
-----END PGP SIGNATURE-----
Reply all
Reply to author
Forward
0 new messages