A formally proved implementation of the inner sandbox validator

[Alexandre Pilkiewicz]

Dear List,

I have been told that my previous messages were not exactly clear
(sweet euphemism), so I come back to you with something hopefully
better (but longer...)!

Short version: I have written and formally proved in Coq
(http://coq.inria.fr) a reduced version of the Native Client
validator. This proof of concept can be found at
https://github.com/pilki/FPdNaCl .

Longer version:
For those of you familiar with the Native Client technology, you can
perform a "goto START_TECHNICAL_EXPLANATION".

Google Native Client is "a [...] technology that allows you to build
web applications that [...] execute native compiled code inside the
browser". It offers two main services. First, a portable API and
custom compiler for the programmers of native applications that will
run inside browsers. The second is a protection for the users of those
applications: with this protection, you can safely download and run a
native application from an untrusted source, without fear for the
integrity of you computer and data.

This protection is what my work is about. For more safety, this
protection has been designed in two layers. The outer sandbox
(currently handled by the Chrome browser) is OS dependent, and deals
mostly with security policies like "which file can I read and/or
write", "which URL can I access", "what OS function can I call"
etc. The inner sandbox (the one I'm interested in) is processor
dependent and is basically here to check that the executed program
cannot bypass the outer sandbox.

This inner sandbox is a validator: it looks at the binary code of the
application and checks that it cannot bypass the outer sandbox, by
directly calling an OS function for example. Sadly, simply
disassembling the code and checking that there is no bad instruction
is not enough: x86 has variable size instructions and imposes no
alignment. It is then possible to write a code that, when decompiled
from a given address (the start of the code segment), contains only
harmless instructions (like additions, jumps, etc) , but that actually
behaves nastily (by calling the OS, reading files, opening sockets,
etc) when executed from a different address. The code can just perform
a jump to this address, and then leak information or corrupt the
system.

The idea behind the native client validator is to check that such
jumps to unchecked addresses are not possible: direct jumps must point
to checked addresses, and indirect jumps must be masked so that the
destination is known to be at an address that is a multiple of 32. The
disassembler also checks that no unsafe instruction can be reached
from those addresses.

START_TECHNICAL_EXPLANATION:
How can we be convinced that checking those properties is enough to
ensure the safety of the application (remember that we are downloading
this application from a completely untrusted source)? The initial
paper _Native Client: A Sandbox for Portable, Untrusted x86 Native
Code_ [1], presenting native client contains a short hand and paper proof
of the algorithm. This proofs suffers two main flaws: first, it is
fairly informal, and second, it is a proof of a pseudo-code algorithm,
not of the actual implementation.

To support my claim that the proof is informal, one can notice that
the implementation of is_2_inst_nacl_jmp_idiom (page 5, figure 3) is
not detailed. It is only called once, with IP (the address in the
code) as the only parameter. One might then think that it is
implemented as "get the previous 3 bytes and check it is the proper
and". This would obviously be incorrect. In fact,
is_2_inst_nacl_jmp_idiom needs to have access to the previously
*parsed* instruction, and such an instruction is never saved in the
pseudo code.

The second flow is the distance between what is proved (a 12 line
algorithm) and the real implementation (more than 50 000 lines,
according to sloccount). Those 50 000 lines contains printing, error
reporting, unit tests, etc. so the multiplicative factor of 4000 is
not fair, but the implementation is still way more complicated than
what is proved. And in particular, it does not follow exactly the same
approach. The fact that the nacljmp (the jump protected by a mask)
does not overlap a block is checked in a second phase for
example. Some bugs (either "logic" bugs, or just implementation bugs)
could have been inserted in the process.

One solution to those two flaws is to use formal methods and in
particular, for the work I'm presenting, the Coq proof assistant
(http://coq.inria.fr).

To quote the website, "Coq is a formal proof management system. It
provides a formal language to write mathematical definitions,
executable algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs." In other
words, it allows you to write programs and to prove strong properties
about those programs, giving you mathematical certainty that your code
works as you intended it to.

How does it solve the problem? First, the proofs are checked by the
machine. This means that special or corner cases cannot be forgotten
(Coq is really, really serious about that!) and that no approximation
can be done (an implementation of is_2_inst_nacl_jmp_idiom must be
given and cannot be left informal. Coq won't let you try and fool
it). This makes the proof way more reliable than a pen and paper one.

Second, the proof is made on the actual code that will be executed. It
removes the possibility of bugs introduced after the proof.

What did I actually implement and prove? My implementation/proof are
parameterized by an assembly language. (For those of you familiar with
ML, i used a functor. For those with a C++ background, it is very
similar to a template). This means that they are generic and can be
instantiated on several assembly languages. For the real world, the
proof is in fact valid only for x86 32 bits (because it assumes the
existence of the segment mechanism), but the parameterized approach
allowed me first to not deal with the full x86 (I only had around a
week and a half to spend on this small project) and second to simplify
the proofs by focusing on the important properties.

This assembly language comes with a formal semantics. A formal
semantics is a definitions of what step of execution can be taken. More
formally, the state of the machine is represented by a memory (an
array of bytes), a program counter (pc) and a set of registers. A step
of execution consists in reading the instruction in the memory found
at the address pc, and then execute it, for example by performing a
jump, a function call, a memory load, etc. (I also added that in
between two steps, the memory can be arbitrary modified except on the
code segment, to simulate multi-threading). Some situations can lead
to a particular state, called DANGER_STATE. This happens when no
proper instruction can be read from the memory (this allows to use a
white list: all instruction not listed are considered dangerous), or
when a bad instruction is executed (like a call to the OS).

From this definition, we can specify what we want to prove:

starting from an initial memory containing the validated code (and
anything in the data segment) and a pc at the start of the code
segment (or in fact at any address multiple of 32), it is *not*
possible to reach a DANGER_STATE, whatever the number of steps
is. This rules out any possibility to jump in the middle of a pair of
mask/jump, any call to the OS, any risky instruction, etc.

I would like to emphasize again that this proof has been made on the
actual code, and not on some pseudo-code, and that it is
machine-checked, making it impossible for me to have made a mistake.

I then instantiated my validator on a toy assembly language, to check
that the hypothesis were realistic. For a real application, it would
need to be instantiated on x86.

So is it 100% sure to be 100% bug free? Like every formally proved
stuff: it is as correct as its specification is. The semantics of the
assembly language must be correct. If a trap in the system is parsed
as an ADD, the validator will obviously be wrong. The specification
must also be complete. Is it all we want that a wrong state cannot be
accessed or is there something else? Finally, some glue has to be
written in ocaml (and not proved), like the transformation of each
segment in a stream of bytes that the validator expects as an entry,
because Coq is a pure language. This glue consists in 12 lines of code
plus 256 lines of automatically generated conversion between two
representations of bytes. All this constitutes the trusted code base
(TCB). It is worth noticing it is way smaller than the current TCB of
NaCl, and that it can be shared by other projects that would need a
formal specification of x86 assembly for example, maximizing the
reviews and minimizing the probability of errors.

A common question is: "what about the performances?" My validator is
currently around a hundred times slower than the C implementation. It
is too slow to be run on production, but this validator has been
implemented and fully proved in only a week and a half. With more
work, it would be possible to crush execution time, using some new
features of Coq, like persistent arrays and native integers.

Finally, is it available? Of course! You can find it on github
https://github.com/pilki/FPdNaCl

To just compile the validator and run the tests, you will only need
ocaml (apt-get install ocaml). To actually check the proof, you will
need the Coq proof assistant. This is detailed in the INSTALL file.

Cheers

Alexandre Pilkiewicz

[1] http://src.chromium.org/viewvc/native_client/data/docs_tarball/nacl/googleclient/native_client/documentation/nacl_paper.pdf

[Ivan Krasin]

Hi Alexandre,

I've tried to checkout your work and run tests. Everything works
smooth. Then I've decided to modify block.tst to check your validator.
I've just doubled the contents of block.tst and I've got that
megablock.tst does not pass the validator. Unfortunately, the
validator does not show the reason of rejection, so I just dump what I
have:

krasin@li139-230:~/formal/FPdNaCl/test/oktests$ cat block.tst
nop 25 ; 25 bytes
%1 <- %2 and 42 ; 7 bytes
djmp 65536
krasin@li139-230:~/formal/FPdNaCl/test/oktests$ cat megablock.tst
nop 25 ; 25 bytes
%1 <- %2 and 42 ; 7 bytes
djmp 65536
nop 25 ; 25 bytes
%1 <- %2 and 42 ; 7 bytes
djmp 65536
krasin@li139-230:~/formal/FPdNaCl/test/oktests$ ./alltests.sh
Check file block.tst
The code has been validated
Check file djmp.tst
The code has been validated
Check file maskjmp.tst
The code has been validated
Check file megablock.tst
This code might be dangerous. REJECTED
#############################################
ECHEC
#############################################

Thanks,
Ivan Krasin

> --
> You received this message because you are subscribed to the Google Groups "Native-Client-Discuss" group.
> To post to this group, send email to native-cli...@googlegroups.com.
> To unsubscribe from this group, send email to native-client-di...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/native-client-discuss?hl=en.
>
>

[Alexandre Pilkiewicz]

Hi Ivan

I have to admit, this validator is not really talkative. It basically
only answers yes or no. I'll try to make it give slightly better
answers soon.

For your particular case, the problem is this:

<<<<<<
nop 25 ; 25 bytes
%1 <- %2 and 42 ; 7 bytes (32 total)
djmp 65536; 5 bytes (37 total)
nop 25 ; 25 bytes (62 total)
%1 <- %2 and 42 ; 7 bytes (overlap the 64 = 32 * 2 barrier)
djmp 65536
>>>>>>

An instruction as to be strictly included in a 32 byte block, so that
it's impossible to jump in a middle of it. With 0x07 being the opcode
of the "system call" instruction, if you have say a "djmp 0x07000000"
instruction (5 bytes) starting 4 bytes before the end of a block, then
you can jump at the start of the next block, and get the 0x07 byte,
the calling the OS.

But once again, a nicer error message would really help!

Cheers

Alex

2011/5/6 Ivan Krasin <imkr...@gmail.com>:

[Ivan Krasin]

On Fri, May 6, 2011 at 3:55 PM, Alexandre Pilkiewicz
<alexandre....@polytechnique.org> wrote:
> Hi Ivan
>
> I have to admit, this validator is not really talkative. It basically
> only answers yes or no. I'll try to make it give slightly better
> answers soon.
>
> For your particular case, the problem is this:
>
> <<<<<<
> nop 25 ; 25 bytes
> %1 <- %2 and 42 ; 7 bytes (32 total)
> djmp 65536; 5 bytes (37 total)
> nop 25 ; 25 bytes (62 total)
> %1 <- %2 and 42 ; 7 bytes (overlap the 64 = 32 * 2 barrier)
> djmp 65536
>>>>>>>

Thanks, changing layout definitely solves the issue.

[Alexandre Pilkiewicz]

Hi

I added some nicer error messages. Hope this helps

Alexandre