more
This commit is contained in:
parent
53ebc3bc75
commit
1bc356216f
1 changed files with 10 additions and 10 deletions
20
Home
20
Home
|
@ -26,23 +26,23 @@ change may result in unforeseen behaviour. Additionally, lots of embedded
|
||||||
devices (home router, SmartTV, etc.) do not have a secure update channel.
|
devices (home router, SmartTV, etc.) do not have a secure update channel.
|
||||||
|
|
||||||
Instead of trying to fix these decades-old operating systems, which were
|
Instead of trying to fix these decades-old operating systems, which were
|
||||||
designed as multi-user time sharing systems of the past, we build small services
|
designed based on demands at that time (e.g. time-multiplexed multi-user
|
||||||
from scratch with security in mind, directly on the hypervisor. In
|
computers), we build small services from scratch with security in mind. Each
|
||||||
our operating system, each service is a separate virtual machine with only the
|
service is run as a separate virtual machine on any hypervisor with only the
|
||||||
required code.
|
strictly necessary code.
|
||||||
|
|
||||||
This makes our systems much smaller. The binary size of an HTTP server with TLS
|
This makes our virtual machines much smaller. The binary size of an HTTP server
|
||||||
support in our system is around 4% compared to one in a conventional operating
|
with TLS support is around 4% compared to one using a conventional Linux
|
||||||
system, making the attack surface much smaller.
|
operating system, making the attack surface much smaller.
|
||||||
|
|
||||||
Additionally, we use a safe programming language: a statically and strongly
|
Additionally, we use a functional programming language with static
|
||||||
typed functional programming language with automated memory management. This
|
types and automated memory management. This
|
||||||
reduces the attack vectors: temporal and spatial memory corruption are no
|
reduces the attack vectors: temporal and spatial memory corruption are no
|
||||||
concern anymore. The declarative programming style makes it possible to
|
concern anymore. The declarative programming style makes it possible to
|
||||||
formally verify the correctness of the entire virtual machine with a theorem
|
formally verify the correctness of the entire virtual machine with a theorem
|
||||||
prover.
|
prover.
|
||||||
|
|
||||||
One of our single purpose operating systems boots within milliseconds, and has a
|
One of our unikernels boots within milliseconds, and has a
|
||||||
minimal memory footprint. For client-side features that run in a webbrowser, we
|
minimal memory footprint. For client-side features that run in a webbrowser, we
|
||||||
compile to JavaScript from the same codebase, to ensure consistency. The strong
|
compile to JavaScript from the same codebase, to ensure consistency. The strong
|
||||||
and static type system helps to detect errors early, and enables rapid
|
and static type system helps to detect errors early, and enables rapid
|
||||||
|
|
Loading…
Reference in a new issue