Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/362 Thanks!
Yeah, hello, my name is Honasan, that's
David, and we will talk a bit about
trustworthy, secure, modular operating
system engineering, which we are
currently doing, or another approach
to how to robustly
implement security protocols.
So first of all, the
general question of this talk is,
what is the trusted computing base and
how can we get it as small
as possible while still having some
functionality?
And the trust of computing base itself
is all the pieces
of software and hardware of the system,
which are crucial for its operation.
And if one fails, the
whole security of the entire system
is jeopardized.
So, yeah.
Well, let's look at a
concrete example of the trusted
computing base in this example will take
an instant messaging client.
So as a trusted computing base
of the instant messaging client, the
first half the client software itself
being at some implementation in
some programing language, so that
client software is obviously part of the
trusted computing base, because if it
contains a box, you might be able to
exploit it and to jeopardize
its security.
Then as the next layer, we have the
dependent libraries so the client
might use open SSL unutilized
or any other piece of security,
cryptography library
or XML stream processing
or whatever.
So that is obviously also part
of the trusted computing base,
as we have seen this year with
Heartbleed, which affect that openness
and which affected a lot of different
applications, which all had openness
as well as their dependent
library.
So as a next step, we're
not quite finished yet.
As a next step, we have the graphical
user interface framework, which
is most often used in such a
client, such an extensive
client. And the graphical
user interface actually contains
stuff which parses arbitrary
binary data like pictures
and fonts and needs to render fonts
and so on. And obviously there have been
Boxun picture pausa,
libraries like Lipinsky like
Drapey.
So this is also part of our trusted
computing base grows and
grows even bigger.
So then we have the programing language
it is implemented in or it provides
an interface for plug ins and
that programing language environment,
that runtime is also executed
and must be part of the trusted computing
base.
So if there is a problem
in some programing language, let's
say HP, which has a long history
of problems, or
Java or Ruby or Python or
whichever you like,
but we are not we are not
really there yet.
So we also have the big
C library, which you unfortunately
can't see, but you can see it here a bit.
So the C library is also part
of the trusted computing base because it
is actually there and you execute
it. It's loaded, it's loaded
into memory. And the C
library contains, what, around 2000
subroutines.
So if there's one
exposed and vulnerable,
the whole security of the whole system is
expected. And here on the right side,
you also see the operating system being
at Linux, privacy or whatever
else the kernel which
provides you with the DCP IP stick
and which provides you with.
Hardware device drivers that
also need to be part of or is part
of the truss computing base.
And then last but not least, we also
have the piece of hardware, the
different pieces of hardware, your
device, your hard drive and so
on, which all contains some firmware,
which is part of the truss
computing base.
So it stacks up
and up and the question
is for Enoteca is
what is the weakest link?
Which piece?
Which piece is the most easy
to attack here?
And obviously, I forgot some things
like the compiler needs to be trusted
because if the compiler is an untrusted
compiler, it can just inject some
arbitrary code into your executable.
So what can we do?
I'm here to propose how to
minimize the trusted computing base or
how to get a small trust the computer
makes. And what have we what
what are the different approaches we have
seen in the past?
Well, the first one of the popular
approaches is compartmentalization
to just build the compartments.
And that actually solves the problem.
If there is and if
there is a successful attack, the impact
is low, the impact is small.
So instead of running each server,
all services on one machine, on
one operating system, you just
spread the services to various
different operating systems.
So each service runs in a in a
separate virtual machine or
in a changing environment, which was
one of the first things
developed there.
Then we also have Solaris zones,
the rails and Linux containers, which is
more lightweight virtualization
currently hyp through DOCA.
And on the other side we have the
where you actually only
run the the userspace of
an operating system.
So you shared the very same kernel,
but you execute different C libraries
and different servers
binaries.
Then on the other side we have the
hypervisor approach such
as Xen, KVM or so
for you have a small hypervisor
on top of that hypervisor.
You run all the different Vitra
machines, which are each of it is
a complete Linux Unix
environment. So its its own,
its own kernel, its own device for
its own TCP IP stack and so on,
and hypervisor such as Zenn
used around the world in this
cloud thingy,
for example, at Amazon, easy to use and
Rackspace and so on.
So Compartments is a really nice
approach to limit the impact
of attack of an attack.
But it doesn't really reduce your
trusted computing base.
Apart from that, you separate
the services apart.
Also, the crucial question is, can
I take an escape from
a changed route or a real or a
hypervisor?
So it's part of the trust computing base
and you actually add a bit more software.
So that's the other project, which
is to just
add stack on layers and layers
and layers, because each problem
in computer science can be solved by
adding another layer.
And the problem is your
setup gets really, really complicated,
gets complex and
such layers, for example, stack
protection or firewalls or
intrusion detection systems.
And the problem here is really that
all these layers are also software
and they are part of the process of
computing base.
So they need to be trusted.
And there have been successful
I mean, there have been vulnerabilities
in firewall implementations and intrusion
detection systems quite a bit.
So you actually open up the tech
victor if you had more layers.
So, as I mentioned, piling layers,
David Villa already said all problems
can be solved in computer science by
adding another layer of indirection,
apart from the problem of having
too many layers of indirection.
So, yeah, that's a state where we
are right now.
So the whole system is
wrong.
Let's start clean slate,
get rid of the
old legacy
here so software
systems are complex.
Yes, today's communication
interfaces are complex because
we have a variety of computers
and but fortunately,
the communication is done
via protocols which are more or less
standardized or formalized
by the IETF and so on.
So the API, which we actually need to
implement for a clean slate approach,
is the API of the Internet,
which might be TCP, IP, the
FTP, DNS,
HTP, whatever.
Some security may be less
Zazzle for authentication,
then maybe some get some
age, some EMAP to communicate
with the other peers, with the entire
world, with the rest of the world.
And then another problem
in computers is persistent data storage.
And I'm not talking here about a hard
drive because the hard drive can fail and
will fail.
But I'm talking here more about
a concept where to put data
such that it is encrypted
storage stored somewhere,
and I can actually retrieve it and only I
can retrieve it.
Not everybody else, because it's my
data.
So what are the tools for this clean
slate approach?
Well, Hecker's, our tools,
programing languages and programing
languages have various kinds
of abstraction features.
And then we have libraries.
So stuff which is already there, which we
can reuse.
So consider that the programing language
is the essential vehicle of expressing
a program, and we just dissect an
operating system into its parts,
so radical in an operating
system, architecture can be radical and
thinking how to actually build an
operating system in use in terms of
programing language, which
which we think is the essential
component.
During the rest of this Congress, you
will hear a series of talks on
a string of high-Profile exploits in
security libraries that happen throughout
this year and interesting properties that
they're all connected by actual failures
in the language, more or less so
with the programing, languages are a
basic tool to to ensure
we're building a more robust, stronger
system.
And the idea
is actually to her programing language,
give us the ability to focus solely on
the problem and not on the accidental
complexity of solving it.
So we're within the abstraction
to do that. And we want to achieve code
that is small and that corresponds
to the expression of the solution and
doesn't contain either not really need
the information.
So what we do is use functional
programing.
And the idea is to say,
well, here's a here's an example,
dysfunctional programing.
It's sending a function that
increments the element Bovon for another
function, which operates a realist,
and then using that function to transform
at least into another one.
And it is the Whitsun with
functional programing. You want to have
the program. That's a network of very
small, isolated local functions,
which can be freely combined in various
ways so that you
don't have to suffer from the complexity
of considering which one is executed,
when or which one was previous
or next.
Are these are these four declarative
programing, which would be the kind of
programing we regret to express
the logic of the solution and not
all the steps it takes for the computer
to arrive at the solution.
This, of course, the simplest example,
functional programing we can give it, but
you can't expect us to squash an entire
program in a single slide
on one of the
functional programing approaches is
under defined. Many people have different
interpretations of what it means.
The one we use in our code actually
is statically typed and quite
orthodox functional programing.
So we have the type system.
There has been a suite of languages
relatively recently that
did away with types because unit
tests or something of the type system
is invaluable
in enforcing lightweight
properties.
We don't have a type system such as more
advanced languages, such as, for example,
ADRIS, which can prove properties but
have a type system that can enforce them
if we can see them, prove them
ourselves, or at least see how they hold
and then send them away, hide them
through abstraction and have the support
system propagate that.
Yes. Now everything really holds the
way we've seen in the beginning.
So that system is a very crucial
component to our approach.
It gives us the soundness.
We kind of on a basic level, no, we're
not doing something wrong in another part
of the application.
And another crucial part to this
functional programing thing is
side-effect.
Now there are definitions of side
effects. My favorite example is that
the side effect is your square root
function, which one third the number two
starts completing the square root of do
the stops, goes away, presses
the far missiles button, fires the
missiles, comes back and gives you on one
point for something, something sidekicks
are a spooky action at a distance,
whichever means a chunk of code can
can use to influence or change
the behavior of another chunk of code,
which is not explicit parameter and
the results returning.
So therefore obviously create complexity
and create horrible complexity.
And and
while definitions of what function
programing is very considerable with
respect to whether side effects are
included or not.
Q For example, the entire
functional JavaScript movement we
subscribe to very the
idea here, we don't use side effects
almost ever, and it turned
out that was a
really beneficial decision.
We don't have variables in the code at
all. We just call functions with
different arguments and we don't have
exceptions, even though the language has
both maybe very low quality
and these things linked to component
causation and led to this ideal of many
small functions which can be fairly
composed, exchanged, switched and
and changed as the program evolves
without considering more things
there are going on.
In other words, a functional language
made it easier to reason about the
program, and that was a crucial enabling
factor.
So we have seen the tools that are
available for program, which
was basically the programing language,
and now we propose to have
this clean slate approach.
We just don't have an operating system,
but instead we have unique and
unique elements, specialized
applications.
So it's not a general-purpose system
here, but it's really
a small, specialized Vitra
machine image, which even includes
all the system libraries and
the configuration so unique
just directly can run on nonexempt
itself.
So I will explain
here a bit about Midrash,
which is the research projects
I'm currently working in, which started
five years ago in Cambridge.
It is all a GMAT license
all available on GitHub users, or Kemel,
which is a module of functional
programing language and that
can compile to
then virtual machine image
on arm or
on eighty-six or whatever.
And the size of that Vitra
machine image is roughly two megabytes
here in that example for an HTP
server serving also
sites over.
So actually implementation.
So all the crypto, all the HTP,
all the TCP, IP and all the
layers up to the scheduler and
whatever you think is inside
of that image or is done
by that image.
So how does a mirage work here?
Well, as I said, we have a clean slate
approach here and we just remove all
the layers we feel are
rather legacy and we don't really need
in a customized application.
So we don't claim to build the
general-purpose operating system here,
but a framework how
to build your own services.
And obviously Matinées server doesn't
need a file system.
Why should it need a system?
Why should it need users?
Local users just need
some sort of indication to do updates.
And the other stuff which should
be done is the request
response on Dean eSport.
So on the design, instead of having
the hardware and the hypervisor on
top of that, the legacy operating
system, like a network stack file system,
user process, Kernow threats some
programing language runtime, some
application that binary and some
configuration files lying around
somewhere on some file system.
We instead just have the Mirage
runtime, which is an optimal runtime,
and then the application code right on
top of that. So we don't have a network
seg inside of the operating
system and so on, but we have it inside
of the runtime
by using that and by directly executing
it on on a hypervisor and then
hypervisor, we actually can use single
other space because we don't need virtual
space. Why should we need a virtual
aerospace if we only have one process
and we only have one process while it's
all even driven so we can handle
multiple connections at the same time.
But nevertheless, we don't have a process
management thing going on
and we don't even have a C library in
here in Misrata is we have
no lipsey.
So a huge bunch
of code of of code
which might contain some security
issues is just removed.
Let's talk a bit about modularity and
what I really mean with that.
So modules modules are a
programing language concept here coming
from the Standard Model, which
then developed further to towards
time and model modules
are the composable units assembling
complex systems together so we can
just stick together.
Some modules and libraries can be
parametrized by modules.
And in the end, we have done an
application using all those various
models, modules and a module is basically
an interface, but
inside of him out there is actually
the whole module system is program
language in its own, basically.
So you can actually program inside
of the module system.
And well, what we use
here so inamorata, as we use the
modularity from all Kemel quite a lot,
and that gives us that
we can run the very same application
code using various
systems of various configurations.
So as the first example,
the old Unix circuit process down
here, we have the my home page,
which is the application I'm talking
about here.
So my home page is actually
that stuff I wrote.
And then someone else has written an
HP server called Kōichi to be
here and I can just compile
my home page from it be and
then just run as a Unix TCP
IP socket process.
So as a Unix binary inside
of an already existing 70s
Unix system,
a different compilation.
So I don't need to change any code here.
I'm just using different modules
and I can just have
a Unix userspace
userspace network process using a
top interface so I can just use
the back end and orange beer,
which is the secret I can only
use, and then my own TCP
IP stack and my own Ethernet stack,
which is part of Miraz
and yet GCP
and I can just execute the very
same application code after recompletion.
I can just execute it as a tune
up, as a process which
listens untuned type interfaces
and then as a third alternative, I
can just get rid of the Unix
system and just use it use
then instead of it.
So the only thing I really need from the
Zen is a virtual network interface
that can just compile it with
the with the Zend
UserSpacE or some Zen libraries.
And I end up in a binary, which
is this Vitra machine running directly
on them.
And I didn't have to touch
my my application code
at all. And that is great to
have a modular system because
I can just debug on Unix as
a subprocess and then when I want to
deploy I can just One-Click deploy
on some cloud service or
on my own machine on the Internet.
Small intermission.
This could be bought.
It could be bought too, which is
and I'm a 20
processor, dual core a seven.
And that actually has the virtualization
bits. So we can actually run
Xen on that board and we
run a little narrow in the zero
and then as the gets operating systems,
we can run midrashic.
And that is a great small
board in order to to run experiments
on what about security
inside of the main vault inside of
it.
Then there is this CubeSat
project, for example, and that
was just puts every
device driver into a separate virtual
machine, said compartmentalizes
the different the different
device drivers.
And each idea can be
mapped to a separate machine.
So this is compartmentalization.
And if one driver is wrong,
the attacker can only
get access to that small
compartment.
Well, unless a hypervisor is
broken as well
as the hypervisor is basically a schedule
schedule which separates
the virtual machines and takes care of
that and schedules the machines
inside of the virtual machine inside of
me, as we just have
shared a piece of shared memory for
accessing the packets which come in.
We teach.
We are. We are.
We are then yet networked.
And we can also do interpret from machine
communication by using
shared memory.
That's also done well, initially done
by computers, by the
library.
So what can we do?
What we do have these beby we do
have some basic products like
the HP, HP, the U.S.
I met.
We have a solution for
the storage. We have Irman, which is
a persistent branch Apple store, which is
similar to get but completely implemented
and look him up and composable and
has various back like in memory
or on filesystem and so on.
Then we have transport layer security at
Lezak and since Miraj
voting machines are so small, I mean they
are two megabytes smaller.
So we can just do the entire
deployment we get and we are Gitter
and just store the small
blob inside of GitHub.
And that is also great because if it
breaks at runtime at some point, if we
can just do a binary search like
Engadget, what what broke
it and instead of get we
have this small binary block, but
that is all we just need.
There's no external configuration and so
on.
What about performance?
Well, actually, in terms
of the performance of Misrata,
Russia is on that.
It could be what I was showing earlier.
And it is similar to Linux on our
when we serve for static
HP data, and that is Linux.
And Marussia is running
this virtual machine on
then on
bought the
start time because a virtual machine is
so small, the time is really,
really fast.
It's so fast that you that we
have a DNS server which just
waits for requests.
And when a request comes in and it
replies with the IP
address and then also it checks whether
that virtual machine is running and if
it's not running, it just started up.
And why the other what the client has
requested the DNS
query, and it's waiting
for the answer in order to establish a
TCAP connection.
Our veteran Sheena's already
booted because it would in twenty
milliseconds.
So it is really services on demand.
We don't run all the Vitra machines
at the same time, but only when they
really need it, when we need them.
So let's talk a bit more
about T what is this transport
layer security.
And the reason for talking about that is,
is because we developed this.
You're a transport layer, security stack
for this mirage in alchemic
from scratch.
And this is the most widely
used security protocol since roughly
15 years that has been
standardized
and it is agile.
So instead of having hard
coded key exchange and cipher
method, it actually negotiates
the protocol vision, the key exchange,
the cipher and the hash tag rhythm to
use.
So it is rather
complex or intricate.
There are also four different versions of
Tlas. Well, we didn't implement SSL
version two and three because we felt
like, well, time is over and
there are still as one point zero one
point twenty one point two and upcoming,
there's also tillers of one point three,
which we haven't yet implemented.
The whole issue of a secure
communication is basically how
to authenticate the other peer,
and that is done in using
trust encrypted.
So those CERT authorities
using 509 public key
infrastructures.
And yeah, I'll just
show you the handshake, because our
stack, um,
well, we wrote some
tracing, we had some tracing
features and
within here you see you can see
a sequence diagram of
last handshake, which was just
produced by my Web browser accessing
that website, which is a Web server
I've written using our Okmulgee
Lastic.
And you see here on the left, the client
on the right, the server will make it a
bit bigger.
Yeah, and those dash lines are
unencrypted messages on the wire and
those solid lines are encrypted messages
you can see at the bottom here, several
staff.
So first, the first messages
from the client and the client actually
says send the client hello.
And it says, well, the
version I support, the highest
version, I support Estela's one point
two. Then it sends some nonce
because the client needs some loans in
order to establish secure communications.
Then we have a set of Syphax.
You said the client says,
oh, look here, these are actually all
the different key exchange and encryption
methods I can use or I
implement. And I'm happy to talk here.
And then the client also makes sense
since arbitrary extensions here.
Well, renegotiation extensions
for security enhancements,
then some elliptic curve stuff and so on.
So that is the first packet.
And then the server actually chooses
the server chooses which product vision
and which cipha to pick
and decipher. It contains the
key exchange algorithm algorithm, the
encryption algorithm and the hash
algorithm.
So in this case, the service says,
oh, yeah, let's talk to one point two
years, by the way, my here,
that is a civil suit.
We talk and there is currently
Fumarole Diffie, Heldman using our as
a certificate and a as
260 256
with
a the algorithm.
Then the server also sent over its server
certificate, and that is the ace
and one included 509
certificate, which the client needs to
check at some point.
Then since we are doing a
if we have one key exchange here, we
need to negotiate or we
need to take the homeland
group and so on.
So the server also senseor here, the
Helmand group, the generator, and it's
public over the wire
and then the server ends with the server
helo done, which is well
now I'm done here with my key exchange.
You continue and the client,
the client sends
over. Now it's Stiffy 11.
She wants it verified that the
certificate is okay and the
server piece of the group and so
on is okay.
And then the massive secret is the
massive secret is
the 40 odd forty eight bits of data
which are used to derive
the symmetric and markets.
And then there's the single message
aspect, which was first sent from the
client to the server and then from the
server to the client, and it says from
now on, we just negotiated on some
crypto parameters and some
key material.
Let's use that.
So then then then the connection
switches to to an encrypted
connection and sends over the finished
package packets.
And the first finished is
well, it also contains a hash in
order to authenticate that the
that the key that the whole
handshake, the whole binary data
of the handshake was received
as it was sent.
And there was no man in the middle who
modified the data because it was all
plain text.
And the same is then sent from server
side to the client state.
And then finally, we are on the layer
where we can handle our application
data and application data.
And this case was an HTP
request. But you can see here and that
was sent from the client server and then
obviously in the server ANSYS with the
application databank.
But let's switch back to the slides.
We just saw the last handshake,
the complete a complete handshake of the
last session, which we produced,
first produced and then sent over
the adjacent to the client.
So the server actually
remembered all the all the packets
but were transferred and transferred
them back to the client.
So let's talk about, OK, Multiclass,
that is our office early
2014. And you left Morocco,
Africa, where you started to develop
a clean slate, transport
layer, security stack
from scratch without any
funding.
And it was very
early in 2014.
I flew there on the 5th of January of
this year and they were drawn
later. And it was even before
before. And there were those security
issues this year in various
implementations like go to fail
and Heartbleed and change cyphers
vulnerability and openness
and various others.
I mean, Gnutella has also had some
problems.
And let's talk a bit
about what Kemel tell us.
So I guess, you know, Attila's hipster
business as I was into before Heartbleed.
Yeah.
Now I try to wrap up
or actually go into details how exactly
you think you've just seen is laid out
inside, because that's the important part
here. It's not just thinking, well,
another Tila's, it's like making Attila's
in another way.
So we basically have several libraries
to handle subtests which are involved in
this security protocol.
So we have the crypto library
and we have the CERT library,
which basically passes and validate
certificates and we have
the overall DELYS built on top of that.
And the crucial part is
that we're aiming for simplicity, but
throughout, inside and outside.
So we want to have the code to the simple
and the code, the not to
be prone to the spooky action at a
distance, to be easier to reason about.
But we also wanted the code to be simple
to use, and it's actually
a published Deficiency of Nonfuel
ASX. There was an actual
published paper about how
the unworldliness of Openness
sells API leads to
in the wild security problems.
And that's because it's called the book,
which is called Back to to Check.
The Certificate's is quite
difficult to implement correctly.
So we're actually aiming to do something
really simple spot on and
as small as possible for everybody
involved.
And we have a few libraries
to do that. And probably the most
interesting one, like below the
Telus level is the crypto
library. And it's also the most
the one most difficult to defend because,
well, you just never developed their own
crypto, right?
We had to because it has to run on Miraj
and it had to be mostly no Camil.
So this then all the crypto
library and
well,
the essential trick
was to try and and not
drown ourselves and the potential
timing channel attacks, other than the
basic correctness, which is not horrible,
difficult to achieve is actually
surprisingly simple. To achieve, we
have to be mindful of all the other
problems that crypto library
can be plagued with.
I might expand on that later on if
anybody's interested in one on
one talk or something.
But as far as timing side channels
and garbage collectors go,
the trick was to separate the
computation, have the very cipher, of
course, the very cryptic course in sit
still, the void of
amplification of the timing differences
through the garbage collector.
So that's our basic defense.
What are we doing? Implementing.
A.K.A.
the timing, crucial parts are
not the camel, but most of the complex,
however, logic is, and that proved to be
simplifying, very much simplified.
So, yeah, we have
we don't really have much crypto yet, but
we have what was necessary to support
our tools.
And lighter note, that has been like
for kicks, we have an RPG
which is thought to be strong.
Entropy sources are still debated
on, but at least there have been mixed.
Well, we have a few
public Kikki algorithms.
We have the basic core block cyphers
that spreads and the Reindl as
and basically through this was for
testing. So we have Reindl and
we have a bunch of hashas which do show
families and the fire and
the separation is always the same.
Ah, with, with the block at things
the block operations are in c always
for speed and to avoid going through a
garbage collector or the
Republican Krypto is in old Camil and
it is very nice to write it in O'Carroll
because each single algorithm together
with all the utilities and then it is
about how many lines of code and very
stretched wide.
So it's nice environment to code in.
Yeah.
And we also have this Essel every now
and then is the same encoding
basically does develop in the early
eighties by telecom industry and
shows and it's
it sounds very abstract syntax notation,
which means that it's it's
a language that defined the structure of
data and then have the on the wire
encoding of data, the automatically
derived from the structure it actually
prescribed encoding wants to give it the
structure and it's a snippet of it.
I'm not going into detail that looks
its language in its own right and be
completely relevant.
It's only used for cert then I think one
other message type in the Telus
handshake. So it wouldn't be interesting
if it wasn't a notorious
surface attack vector in
the past because the former district
of Pass and very often
the other libraries don't pass it
safely.
So now and again
of bed exploits
are precisely in their celaya
to this Dasan
the solution to our son.
Yeah, we have something pasada.
There is something to focus on the
snippets of code, the previous
one and the next one.
So he'll go over the surface
index was slightly different.
What connects those?
Not a lot of thinking
and it is that we have an embedded light
because an account the outcome
is a very nice language to embed other
languages in.
So instead of going in, doing all the
passing that's usually been
done, just step aside, solve
the problem of passing in isolation,
and then build language like this to
express what they actually need to be
passed in the crypto context.
So this is one of the one of the examples
where there's a camel actually shiz to
separate concerns.
We also have the library that delivered
certificates, which might actually be
extended the soon to to to be
a standalone utility for or for
various things to want to do with your
certificates.
And
maybe the most interesting thing to note
is the simplicity of Teppei.
Essentially, we have two ways to
construct something that authenticates
your certificates.
And we implement the standard chain of
trust where you
provide the library with a certificate,
the roads and certificates,
and it can be queried
with another certificate and or
certificate stack and check itself, pass
by letters and everything and check the
chain whether your certificate
authorities actually did sign
the chain ultimately.
And they also have another kind of
checking built in, which is checking
off fingerprints, which can then
be accumulated, which is the basis
for trust in the first use mechanism.
So these are the parts and
then there is the topmost delays.
And this is a mouthful, definitely.
But what's to say is that the
DOE Network library you've
just seen in action boils down to
two anthropoid functions, nothing more
to one function to to process that
data that came from the outside and
other function to process data, which is
to be sent to the outside.
And it's more or less at
the time. Signature of the first one
itself is still multiple.
But it was the real one to say is that it
takes two things
into three things.
It takes whatever describes the state
of the session in progress
and a by tractor and
produces the next state after processing
the tractor, maybe by a factor
which is intended for the application to
resume, and maybe a third by vector,
which is the immediate response.
And that's all.
It doesn't do anything else.
It doesn't even keep state.
Its state is a value, just a description
of of a session in progress, which
you can actually store and provide back,
get out of sync with the other end point.
But you can do that.
And as for sending, it's also incredibly
well, just one little
it up there into triple,
but not exactly.
It lets it there into either a triple
or a value that describes an error.
So they are handling is completely
localized in that return value is
completely explicit. If you want to run
it, you have to check if there was an
error. It's very easy to do
that. That kind of simplicity aiming at
and the their function is essentially
give it the state and then give it to a
bunch of byte vectors to process and it
will give in your state and something to
send over a letter.
So this entire
apparatus of doing
the protocol is.
Contained in a
pure bit of code, doesn't even know about
sockets, it doesn't know about state.
It doesn't know about network.
You know about almost nothing.
It just takes some values and computes
some other values.
And that's a really good position
to be in when writing a security
protocol.
And of course, you don't want to use that
directly. So that's the core.
And then we have some.
Then sends some top of that, which
actually give you more or less idiomatic
interfaces to work with for various
libraries that the person might use.
No, Colonel, this, for example,
one this is one example where you can
accept the connection of the private
material and a file descriptor and get
the pair of channels to communicate on
and the address of the other end point
and relatively similar to the
function that you give it, the phone
notification of the difficulty which you
somehow synthesize the other end point
and it connects.
This is not important. What's important
is that if you have a completely pure
core, not only you can reason about it,
you can also glue it into whichever
context you want.
This is one of the links we have either,
and this is not even the main one,
because this is not the API we can
manufacture, however, many
of those we want, because incredible
flexible not to have an interaction with
the outside world.
So what is the status of all
camel?
Well, I just showed you this, the
last handshake and that was running on
our own t stack on the
server side.
And we have that demo server life
since July ursu this year.
And we served over 50000 sessions
and we successfully serve them.
So we have interoperability with
a lot of different elastics.
Well, unfortunately, there aren't that
many tools out there.
And we managed to develop a
working tea lasting and a robust
implementation off at the last stake
in a very short time frame, and that was,
what, January of this year when we
started. So less than three months
to work on implementation?
Yeah, roughly three months to to
do that. And while doing that, we
reflected a lot of times our entire
code base and we learned a lot
about how to securely
write or how to write
robust implementations of security
protocols inside of a functional
programing language which has Petten
Metric basically and
the statistics life.
Just use your sealant for line
counting. And I just counted the entire
repository. I didn't strip out anything.
And openness to sell has roughly
350000 lines of code.
Well, fortunately, they are the liberals,
the guys who managed until
well within a few months to strip
out at least fifty thousand lines of that
code.
So that is a great approach
to sell another small
sea base
implementation is roughly 100000
lines of code.
Our code bases currently
20000 lines of code.
And we can operate and we have
nearly all the features we actually
need to have.
And also, well, they even operability
here as shown for the server side, but
also the client side works with various
different stacks.
What is the future?
Well, we already have some
preliminary pull requests
for client authentication data deciphers
and server side server name
ID configuration.
What we currently don't have code for is
secondary resumption and elliptic curve
crypto cryptography.
We might plan to do
that or not. It's not that
hugely important, I think,
but we want to move forward now.
We have a healthy, functional code
base, which is rather easy to extend,
and we actually extended it by
developing al-Attiyah in
a very short time frame.
In order to do that, we need a D
a support in no crypto and that was
done within less than a week.
Our own implementation
currently doesn't have doesn't implement
the socialist millionaires' problem for
authentication,
but that is only a simple
matter of programing now and
then.
We also have this or Kemel Telus
is now exposed to all
or Kemel applications that want
to use it even.
We are a framework which is called
Convit, which is which
abstracts over the various kinds of
connections you can have.
So either shared memory or
TCP or tearless or
whatever.
And the Conrade Library is just
both server and client site
and abstraction over that.
And you just say, oh, I want to talk
to that host.
And if it's on the same
hosted the same physicalness, you can
just have a virtual machine,
virtual shared memory
connection.
And in December, so this month, they
also implemented Tech Line,
which is a command line client
using our
Otar library, our Telus Library
and so on.
So there is not much C-code
in this direct line because
yet only command line.
And you can see a screenshot I don't
have at the moment an Internet
connection, but I'm happy to demonstrate
to you.
And what is the trust trusted code base
in our scenario?
So I started this talk with the trusted
code base and I want to also
conclude what the trusted code base of
line of my instant messaging client is
Follett's then hypervisor, because it
runs on Zen.
And on top of then we have a library
called Mini US, which provides
you with some sups and
print functionality.
Then we use open lip and mouth to mouth
library. We use noodles
for the big emetic.
Then we have the all runtime.
So the or Kemel
though Campbell programing language
runtime, which includes a garbage
collector and so on, that we have various
will come a library which which we
commonly use like Seasprite, which is a
butt bite vector and so on.
Next 597 one
Otara no to
the library itself and so on.
And then obviously we also have the
compiler, Kremlin C compiler, but
we don't have any lipsey in here
in the trusted code base or any huge
Linux kernel because we just
don't have it.
So to conclude
the stock, I think functional operating
systems are real now.
I use it. I use decline
as my day to day and copy client.
You might ask why.
Okay, well, because
Mirage's was there, but there are other
approaches, other unique kernel based
approaches in Haskell called Helvey
and there's Airlangga and then so you can
execute directly along on the machine
and I believe legacy and traditions.
Let's start to build secure and resilient
systems we phased
out.
And in Germany, we managed to
phase out the nuclear energy by
2022.
And that's also 70s technology
that's similar to Genex.
Let's phase out Unix as well.
And that let's keep it simple
and the complexity is always the enemy
and remove the layers of abstractions
which we don't need any longer.
And so join our new Lipsey
movement.
We also need help.
Try it out. Try Midrash.
All right.
Kate ordered the code, break the code,
discussed the code pieces you are
interested in with us here at
the Congress.
I'm up there at the coffee nuts area
and I'm happy to serve you some
espresso.
While we talk about midrash and
functional programing,
let me thank some people involved.
There's first and foremost, there's
Mother Fedi who started this
whole project back in 2009.
Then I also would like to thank Peter
Sewel. He's a nice guy.
He will also talk.
He is not here yet, but he will talk on
day four at
the same time in the other room about why
computers are so fucked and what we can
do about it.
And then lots of various other people
and all the people I forgot.
So that is our talk.
And we are happy to take questions and
answers.
OK, thank you very much.
OK, I said we have about 10 minutes left
for a question Q&A, so please,
we have all the way as always, we have
six microphones in the room.
Please line up behind the microphones for
people on the stream and on the Internet.
We also have a signal angel in the room.
We can put we can ask your
questions in room. So please write them
to question the I.R.S.
on Twitter wherever.
And they will get asked the
first question, please, from microphone
number three.
Oh, uh, yeah.
Thanks for the talk.
We're cool. Um, I was wondering
if you lose most
of the filesystem stuff and all that,
which usually gives you some entropy.
Where do you get the reform and
reduce of?
You don't really get the entropy from the
file system.
You get entropy from anything
you can get entropy from.
So get it from Interbrand timings,
you get it from your Sibiu.
You get it from your.
I think actually it
is, yes, it is, and gathering
anthropos beside the fact, but so is
using it.
And I think we didn't fashion the
structural IT random number generation
is a side effect that's retained.
We do that side effect.
Sorry. We're sorry.
Well, I'd go home, but
to answer that question, so inside
of the Zen domain, inside
of a virtual machine, inside
of Zen, we actually wrote the host.
So in zero we still have some
Unix legacy code and that
one feeds some of its entropy
to the Vitra guests.
So we wrote a device for that,
for doing that and for communicating the
some entropy into the virtual machine,
because otherwise we are rather low
on entropy.
OK, we take two questions from the
Internet, please.
Yeah, OK, so the first question was asked
quite some time ago, so I'm not quite
sure if you've already talked to
that.
Someone asked how do you account for box
and the underlying layers like then
do you want to isolate those layers to
what about Hata vulnerabilities,
not vulnerabilities?
Well, at some point we have to start
and starting from scratch
with nothing.
I don't think my lifetime is enough for
that. So we decided to start somewhere
and currently we trust
the hardware, but hopefully more open
borders and so on will develop
so we can actually verify or do some sort
of verification of hardware.
And also the same story is true for the
hypervisor. There are various projects to
start to verify the correctness
of hyperbolizes, and we're happy
to switch over to another
back and forth for new upcoming
hypervisor.
OK, so that second question was that
as far as I understand, you don't verify
your code, is that correct?
And how do you test your code?
So that is correct.
I did my dissertation informal
verification of object oriented code,
where we fought a lot about
mutable states and
that was also tedious to to verify.
And currently we just write it
down. It looks in
this declarative approach, it looks
really readable.
And you can actually read the statement,
read from it.
And for testing, we have
obviously interoperability tests, some
unit tests, and we are also developing
we are working on a test environment
for especially those
protocols.
Yes, I can expand a little bit on that.
The next project we're supposed to do is
actually a very comprehensive test
for dels.
So it's through. We don't do a verification,
but it's a long story.
It's not really clear what to verify at
all. There is a very fatalistic,
but they're very sacred.
The soundness of Delys, the protocol,
it's not clear what to verify at all.
And we don't use the system that would
allow us to do that.
But we are just about to do
a very large test silvertails.
So if you give me a specification,
a formal specification of tearless, I'm
happy to verify.
OK, next question from microphone number
two, please.
Hi.
So do you have plans
to have them zeer written in Akana
or as a unique.
That's the first question.
So you and Colonel Seconders,
do you have plans for a
targeting desktop systems, so
specifically doing
gooier virtualization, using
or whatever you want to use
in that case?
Last question. What and distribution
do you use personally to use your as
you said, you use unique
Col's to run your Javor
distribution is so in order?
No, we don't have a Dunsborough and come
on, do you plan?
Not right now, because actually
that's a very interesting question.
Niraj follows up on a tradition of
so-called liberal operating systems which
were built and XO Col's, which means that
the kernel only provides for separation
and isolation, but not for facilities.
I think there are three of those systems.
All three failed due to the difficulty
of providing comprehensive drivers
support.
The trick with MERAJ is that the
transcendant and the trick with sand
is that it runs Linux and Alpro
as Linux, but with access to your PCI bus
and the rest to get drivers.
So more or less right now, no,
we don't have a plan to build them zero
in on because we would have to cover
all the hardware it could possibly run
on, assuming we can get rid of
almost all the drivers from zero.
Would that be feasible then
if we could have if we could get rid
of most of the drivers in zero?
So including Deepu,
would it be feasible, do you think?
It probably would be feasible
to implement DOMS zero for
the management domain in that case,
yes.
For something really small, we don't have
a concrete plan.
In principle, it would be feasible, but
it would be tied to a particular piece of
hardware, like a particular on board.
That's the trade of zero, a
general-purpose one gives the
hardware.
OK, the next question was, do you have
any plans for GUI applications?
So like desktop applications, web
browser, etc.?
Um, not not right now.
I'm working on this exemptive decline,
which is all command line based.
And at the moment I'm mainly interested
in that because I think that the
graphical point and use point
and click interfaces, that that is
a huge amount of work to to implement.
And we are currently mainly focusing
on command line and server side
and lots and distribution.
Do you use for your for
your use personal use arch Linux.
Well, I use privacy.
OK, thank you.
OK, we really have to microphone to
someone else and make sure no one is
coming back to white lights and
state.
How do you deal with time inside channels
in your crypto library?
Because if you reimplemented so
fast you are begging for
new time inside Chestnut's and
Clip-Clop is not
designed for
constant execution time of
large, no multiplication
and some use even
time inside channel information in there
multiply instructions.
So yeah. So Lepchenko was not designed
for a constant time, of course, because
essentially saying Konstantine
Dignam operations is like saying
Konstantine string length without
the length felt.
But at that level there
obviously operations were a good size
and that level with the blending
traditional countermeasures which are not
in the constant time primitive
Artomatic operations, but.
There are higher up algorithmic level
like RSA blinding this and blinding
is still not clear in
details, but.
Where timing leaks have presented
big name code, which is blinded by
the usual methods, and I
honestly didn't didn't hear the first
part of the question we're asking about
timing aside channels in Low-Level cipher
code.
If I understand you correctly,
you reimplement at Mosiah first in
Okemah?
No, that's the trick of actually use
the reference implementation of Reindl in
C we did not reimplemented.
We should switch it at some point.
Avoid the cash based
index of Arae timing Leakin
Reindl. But right now we have the actual
code signed by the original
authoress of Reindl.
The trick is that the code has unrolled
around loop, no allocation
and just straight forward.
So that's what tinsy everything else is
all kemel. We didn't implement them
precisely not to do Nasta
mistakes.
OK, thank you.
OK, a quick question from microphone
number two please.
I don't really understand why you think
that the OS will be more secure than
Linux or Windows because
now it's a toy OS to have not much
code. OK, but sometimes it
will be a feature complete and then it
will be Eco-System Free PC or
Linux.
And just using Okarma will not
make your code secure by default.
So in know, Carol, we have
some language features that
prevent certain sorts of attacks
like overflows because we don't
have many memory management inside of,
OK, so there's a whole area
of Backes which we actually prevent
and the other protists that instead
of having thirty three hundred
fifty thousand lines of code, we are
currently at 20000 lines of code.
Yeah, it might, it might
double to be at
the same level of features, but then it's
still a factor of 10 smaller than
openness.
So I don't believe
that because
I'm reviewing code
written in OK is much more difficult
than say a cowritten see
and see.
Yes, it is actually
actually the propolis or that question.
We should compare in detail
the code for the
tasks or regions that were affected by
last year's high profile exploits in
other Krypto libraries.
And the contrast is more than stark.
Something like Heartbleed
constitutionally cannot happen at
all. Not yet. The GC did the memory
safety because we can't reinterpret
a key as a buffer or a vector.
On the other hand, there is some logical
bugs like Chainsawed Forsooth, which is
which is not quite
quite a bit of bugs in open air.
So this year, which is a problem
in the unwieldiness of encoding
the state machine in C,
and if you just see look at the
difference between code and how obvious
this problem is, there are no gammel
implied they are. And see, I
think you would us.
Everything's OK.
OK, I'm sorry, but we ran out of time,
so please again ask you for one more
round of applause for Honasan, David, for
Go Talk.
Thank you very much.