-
Notifications
You must be signed in to change notification settings - Fork 14
/
Copy pathREADME
355 lines (273 loc) · 13.4 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
The Muen Separation Kernel
==========================
Muen is an Open Source separation kernel (SK) for the Intel x86/64 architecture
that has been formally proven to contain no runtime errors at the source code
level. It is developed in Switzerland by https://www.codelabs.ch[codelabs
GmbH]. Muen was designed specifically to meet the challenging requirements of
high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable
for highly critical systems and advanced national security platforms, codelabs
closely cooperates with the high-security specialist secunet Security Networks
AG in Germany.
image::doc/images/example.svg[Example Architecture, width=70%, align="center"]
A separation kernel is a specialized microkernel that provides an execution
environment for components that exclusively communicate according to a given
security policy and are otherwise strictly isolated from each other. The
covert channel problem, largely ignored by other platforms, is addressed
explicitly by these kernels. SKs are generally more static and smaller than
dynamic microkernels, which minimizes the possibility of kernel failure,
enables the application of formal verification techniques and the mitigation of
covert channels.
Muen uses Intel's hardware-assisted virtualization technology VT-x as core
mechanism to separate components. The kernel executes in VMX root mode, while
user components, so called 'subjects', run in VMX non-root mode. Hardware
passthrough is realized using Intel's VT-d DMA and interrupt remapping
technology. This enables the secure assignment of PCI devices to subjects.
NOTE: Muen is under active development and verification of kernel properties is
ongoing.
Features
--------
Kernel
~~~~~~
The following list outlines the most-prominent features of the Muen kernel:
* Minimal SK for the Intel x86/64 architecture written in SPARK 2014
* Full availability of source code and documentation
* Proof of absence of runtime errors
* Multicore support
* Nested paging (EPT) and memory typing (PAT)
* Fixed cyclic scheduling using Intel VMX preemption timer
* Static assignment of resources according to system policy
* PCI device passthrough using Intel VT-d (DMAR and IR)
* PCI config space emulation
* Support for Message Signaled Interrupts (MSI)
* Minimal Zero-Footprint Run-Time (RTS)
* Event mechanism
* Shared memory channels for inter-subject communication
* Crash Audit
* Support for 64-bit native and 32/64-bit VM subjects
- Native 64-bit Ada subjects
- Native 64-bit SPARK 2014 subjects
- Linux 32/64-bit VMs
- SMP for Linux VMs
- MirageOS unikernels <<mirageos>>
Tau0
~~~~
_Tau0_ (τ₀) is the Muen System Composer. In its current static mode of
operation, the task of Tau0 is to compose a system image while making sure that
certain invariants are not violated. The Tau0 concept is a mechanism to
gradually increase the flexibility of component-based systems running on top of
Muen, while keeping a high level of assurance regarding the correctness of
isolation enforcement. Read more about Tau0 https://muen.sk/tau0.html[here].
Components
~~~~~~~~~~
The Muen platform includes re-usable components which implement common services:
* AHCI (SATA) driver subject written in SPARK 2014
* Device Manager (DM) written in SPARK 2014
* Subject Monitor (SM) written in SPARK 2014
* Subject Loader (SL) written in SPARK 2014
* Subject Lifecycle Controller written in SPARK 2014
* Timeserver subject written in SPARK 2014
* Debugserver subject written in Ada 2012
* PS/2 driver subject written in Ada 2012
* Virtual Terminal (VT) subject written in Ada 2012
Furthermore the <<muenfs>>, <<muennet>> and <<muenblock>> Linux kernel modules
provide virtual filesystem, network interface and block I/O drivers based on
inter-subject memory channels.
Toolchain
~~~~~~~~~
The Muen platform includes a versatile toolchain which facilitates the
specification and construction of component-based systems in different
application domains.
The <<mugenhwcfg>> tool for automated hardware description generation simplifies
the addition of support for new target machines. There is also a Debian
Live-based bootable image <<mugenhwcfg-live>> with persistence to simplify the
collection of hardware configurations from new targets.
Resources
---------
Documentation
~~~~~~~~~~~~~
The following detailed project documentation is available:
* Muen System Specification +
https://muen.sk/muen-system-spec.pdf
* Muen Kernel Specification +
https://muen.sk/muen-kernel-spec.pdf
* Muen Component Specification +
https://muen.sk/muen-component-spec.pdf
* Bootloader Signed Block Stream of Commands Specification +
https://muen.sk/bsbsc-spec.pdf
* Original Muen master thesis +
https://muen.sk/muen-report.pdf
* Muen project presentation +
https://muen.sk/muen-slides.pdf
* Presentation given at High Integrity Software Conference HIS 2014 +
http://www.slideshare.net/AdaCore/slides-his-2014secunethsr
* Technical articles on Muen +
https://muen.sk/articles.html
Mailing list
~~~~~~~~~~~~
The [email protected] mailing list is used for project announcements and
discussions regarding the Muen separation kernel.
* To subscribe to the list, send a (blank) mail to
mailto:muen-dev+\[email protected][].
Note: A Google account is *not* required, any email address should work.
* To post a message to the list write an email to [email protected].
* The list has a Google Groups web interface:
https://groups.google.com/group/muen-dev.
Download
--------
The Muen sources are available through the following git repository:
$ git clone --recursive https://git.codelabs.ch/git/muen.git
A browsable version of the repository is available here:
https://git.codelabs.ch/?p=muen.git
A ZIP archive of the current Muen sources can be downloaded here:
https://git.codelabs.ch/?p=muen.git;a=snapshot;h=HEAD;sf=zip
NOTE: The ZIP archive cannot be used to build the example system since it does
not contain all sub-projects.
Build
-----
Environment
~~~~~~~~~~~
The Muen SK has been developed and successfully tested using the development
environment listed in the following table.
|===================================================================
| Operating systems | Debian GNU/Linux 12 x86_64 +
Ubuntu 22.04 x86_64
| Linux kernel/KVM | >= 5.2.0 with GUEST_CR3 fix <<lnxcr3>>
| Ada compiler | GNAT FSF 12.2
| GCC version | gcc (GCC) 12.2
| SPARK version | 12.1
| Emulator | qemu-system-x86_64 (>= 3.1.0)
| Intel AMT SoL client | amtterm (>= commit 0ece513...)
| Intel vPro AMT / WSMan | amtc (github.com/schnoddelbotz/amtc)
|===================================================================
The following hardware is used for the development of Muen. There is a good
chance similar hardware works out-of-the box if the microarchitecture is Ivy
Bridge or newer.
|===================================================================
| ASUS Prime Z690-P D4 | Alder Lake | i5-125000
| iBASE MI995VF-X27 | Coffee Lake | Xeon E-2176M
| Lenovo ThinkPad T480s | Kaby Lake | i7-8650U
| HPE DL380 Gen10 Server | Skylake | Xeon Gold 6130
| Lenovo ThinkPad X260 | Skylake | i7-6500U
| Intel NUC 6i7KYK | Skylake | i7-6770HQ
| UP^2^ maker board | Apollo Lake | Atom E3950
| Intel NUC 6CAYH | Apollo Lake | Celeron J3455
| Intel NUC 5i5MYHE | Broadwell | i5-5300U
| Cirrus7 Nimbus | Haswell | i7-4765T
| Lenovo ThinkPad T440s | Haswell | i7-4600U
| Lenovo ThinkPad T430s | Ivy Bridge | i7-3520M
| Kontron Technology KTQM77/mITX | Ivy Bridge | i7-3610QE
|===================================================================
The first step to build Muen is to install the required packages. See the
`tools/docker/Dockerfile.muen-dev-env` file in the project repository for the
current list of required packages.
Muen is built using a GNAT FSF toolchain provided via <<alire>>, see the
project's website about instructions on how to install the `alr` command-line
tool for your distribution. Then clone and build the Muen meta crate for alire,
which takes care of installing and configuring the toolchain:
$ git clone https://git.codelabs.ch/alire/muen-dev-env.git
$ cd muen-dev-env
$ make
$ source ./env
Docker
~~~~~~
There is also a ready-made Docker image which contains all necessary tools for
Muen development. You can install it using the following command:
$ docker pull ghcr.io/codelabs-ch/muen-dev-env
Compilation
~~~~~~~~~~~
To build the Muen tools, RTS, kernel and example components change to the Muen
source directory and issue the following command:
$ make
This will create a bootable ISO image containing the example system. See below
for deployment instructions.
The following command gives a short description of the top-level Makefile
targets:
$ make help
Deploy
------
The build system provides two ways to instantly deploy and test the created
system image.
Emulation
~~~~~~~~~
To ease kernel development and testing, the Muen project makes use of nested
virtualization provided by QEMU/KVM. In order for this to work, a Linux
kernel (>= 5.2.0) with applied KVM GUEST_CR3 fix <<lnxcr3>> and the
`qemu-system-x86_64` binary must be installed on the build machine.
Issue the following command in the Muen project directory to start the nested
virtualization of a Muen system:
$ make emulate
The system serial output is written to `emulate/serial.out`. Follow the
on-screen instructions on how to connect to the QEMU curses console or how to
SSH into the NIC Linux guest VM.
NOTE: As the virtual terminal (VT) over curses is timing sensitive and QEMU/KVM
cannot guarantee tick-exact timing depending on the host CPU and system load,
this console is just an emergency console. Use SSH to interact with the booted
Muen system.
Hardware
~~~~~~~~
The top-level Makefile provides two convenient targets to deploy Muen to real
hardware: `iso` and `deploy`. The first creates a bootable ISO image which can
be burned on a CD-ROM or dumped on a USB stick, the second uses network boot to
shorten round-trips during development.
USB Stick
^^^^^^^^^
To create a bootable USB stick containing the Muen system, enter the following
commands in the top-level directory:
$ make HARDWARE=hardware/lenovo-t440s.xml SYSTEM=xml/demo_system_vtd.xml iso
Then follow the instructions on the screen.
Network Boot
^^^^^^^^^^^^
For fast deployment of the Muen system image to real hardware, the iPXE
<<ipxe>> boot firmware installed on a USB stick in conjunction with Intel Active
Management Technology (AMT) is used. Please refer to the amtterm <<amt>>
documentation on how to configure AMT on the target hardware.
To build and install iPXE with the Muen specific boot script issue the
following commands:
$ sudo apt-get install liblzma-dev
$ git clone git://git.ipxe.org/ipxe.git
$ wget https://muen.sk/muen.ipxe
$ cd ipxe/src
$ make bin/ipxe.usb EMBED=../../muen.ipxe
$ sudo dd if=bin/ipxe.usb of=/dev/sdX
The `/dev/sdX` device is the USB stick (e.g. `/dev/sdc`, without partition
number). *All existing data will be erased*.
When booting from the created stick the first NIC (net0) is configured as follows:
IP Address : 192.168.254.2
Netmask : 255.255.255.0
Gateway : 192.168.254.1
After initialization of the network adapter iPXE tries to download and
chainload the iPXE configuration from the following URL:
http://192.168.254.1:8000/boot.cfg
The development machine must be connected to the target hardware via an
interface with IP address 192.168.254.1. To actually serve the created system
image to the bootloader, issue the following command in the top-level Muen
directory:
$ export AMT_PASSWORD=<your AMT password>
$ make deploy
To view the output of the Muen kernel debug console use the command:
$ amtterm 192.168.254.2
If your hardware differs from the default configuration, additionally specify
the `HARDWARE` variable:
$ make deploy HARDWARE=hardware/intel-nuc-dc53427hye.xml
References
----------
- [[[lnxcr3]]] Linux KVM GUEST_CR3 fix, https://patchwork.kernel.org/patch/11165185/
- [[[alire]]] ALIRE: Ada LIbrary REpository, https://alire.ada.dev/
- [[[ipxe]]] iPXE boot firmware, https://ipxe.org/
- [[[amt]]] Intel AMT SoL client + tools, https://www.kraxel.org/cgit/amtterm/
- [[[mirageos]]] MirageOS, https://mirage.io
- [[[muenblock]]] Muenblock Linux kernel module, https://git.codelabs.ch/?p=muen/linux/muenblock.git
- [[[muenfs]]] Muenfs Linux kernel module, https://git.codelabs.ch/?p=muen/linux/muenfs.git
- [[[muennet]]] Muennet Linux kernel module, https://git.codelabs.ch/?p=muen/linux/muennet.git
- [[[mugenhwcfg]]] Muen hardware config generator, https://git.codelabs.ch/?p=muen/mugenhwcfg.git
- [[[mugenhwcfg-live]]] Mugenhwcfg Live, https://github.com/codelabs-ch/mugenhwcfg-live/releases
License
-------
--------------------------------------------------------------------------------
Copyright (C) 2013-2024 Reto Buerki <[email protected]>
Copyright (C) 2013-2024 Adrian-Ken Rueegsegger <[email protected]>
This program is free software: you can redistribute it and/or modify it under
the terms of the GNU General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.
--------------------------------------------------------------------------------