Information on implementing L4
Andrew Warkentin
andreww591 at gmail.com
Sat Sep 15 04:23:23 CEST 2018
On 9/14/18, John <john.r.moser at gmail.com> wrote:
>
> Those processes with limited hardware access are able to do funny thing.
>
> The process that manages virtual memory, for example, can get into the
> memory space of any process running on the system. It crosses all security
> boundaries.
>
Under UX/RT it will be impossible to load code into either the process
server or the kernel (which will be the most security-critical
components in the system), and both will be based on safer code (the
kernel will be seL4, and the process server will be written in Rust),
so the attack surface will be very small.
>
> If you load a rogue VFS driver, it can take over all file system access,
> injecting code into software and crossing all security boundaries.
>
Not on UX/RT. Filesystem servers will not be able to control the
entire VFS. They will only have control over filesystems they export.
In fact, they will not be able to access the VFS at all as anything
other than a client until another process mounts their filesystems (to
act as a filesystem server, a process will request a "port" from a
special filesystem built into the root server, and then some other
process, usually the mount command, will send a request to the root
server to mount the port on a directory, analogous to mounting a block
device in a conventional Unix).
>
> So imagine if you loaded a malicious network card driver into L4. It's
> running Ring-3, it's passing IPC messages to the L4 kernel and to the TCP
> stack, it has its own memory space, and it's tampering with your connection
> and sending copies of bank data to a command and control server in Russia.
>
Yes, but the malware can't make itself persistent unless it was
installed some other way, since the network stack won't have
privileges to install software. Under UX/RT, only the package manager
or a shell session with the proper administrative role will be allowed
to install software. The package manager will have a "locked open"
verification scheme based on reproducible builds, where multiple
mirrors controlled by different organizations in different countries
will all build the same source from the same commit and sign the
package if the binary matches, which will require all changes to be on
the record, and replacing a verified package with a non-verified one
will fail unless explicitly overridden.
More information about the l4-hackers
mailing list