capnproto / capnproto-rust

Cap'n Proto for Rust
MIT License
2.06k stars 222 forks source link

Reduce the amount of unsafe code #78

Open DemiMarie opened 7 years ago

DemiMarie commented 7 years ago

Currently, the code (especially layout.rs) is horribly unsafe. In fact, it appears less safe than even the C++ version, which uses template metaprogramming to catch overflow at compile time.

While the interface claims to be safe, the amount of unsafe code in the implementation is worrying when security is a concern. Most of the unsafety seems to appear as a result of accessing fields essentially by raw pointer arithmetic. One solution might be to generate a #[repr(packed)] struct type that represents the actual data off of the wire. Accessing this struct is then safe, at least once one has a reference (by necessity shared) to it. Rust provides #[inline] to ensure that the accessors inline away and have zero overhead.

dwrensha commented 7 years ago

Probably the most straightforward way to reduce the amount of unsafe code would be use slices instead of raw pointers. For example, in ListReader, the ptr field could be a &[Word] instead of a *const u8. There are a lot of details to hammer out about how exactly to make this work, and such a change would probably entail some performance overhead, but perhaps the added safety would be worth it.

A more ambitious approach would be to use formal methods. It would be really cool if we had a theorem prover that allowed us verify that the unsafe code does the right thing. The invariants that need to be upheld in layout.rs seem simple enough; mainly we need to verify that the results of various pieces of integer arithmetic stay within certain bounds. With a few annotations sprinkled in, an automated prover should have no trouble checking whether those invariants hold. Unfortunately, as far as I know, no such prover exists for Rust yet. (In fact, part of my motivation for working on seer is to understand what such a prover might look like.)

DemiMarie commented 6 years ago

@dwrensha I have tried to work on this, but I am not even at the point of it compiling yet. Hard part is simply the massive amount of refactoring required.

How good is our fuzzing coverage? If it is perfect, we might be able to conclude that the codebase is secure already, since the Cap’n Proto format should be very well suited to fuzz testing.

dwrensha commented 6 years ago

Our code coverage is certainly not perfect, but we do have some fuzz tests that have been run for days without finding any new bugs: https://github.com/capnproto/capnproto-rust/tree/35027494bb6e741aa478597358bac8ac92108a30/capnp/fuzz/fuzzers

indo-dev-0 commented 4 years ago

A more ambitious approach would be to use formal methods. ... (In fact, part of my motivation for working on seer is to understand what such a prover might look like.)

What's the status on this? It looks like seer is unmaintained, but you added some tests using Miri? AFAICT Cargo Klee and Haybale should be able to reason about unsafe code as well.

DemiMarie commented 4 years ago

@dwrensha what is the code coverage on the fuzz tests?

dwrensha commented 4 years ago

The recent Miri testing mostly had to do with preventing undefined behavior having to do with alignment: https://dwrensha.github.io/capnproto-rust/2020/01/19/new-feature-to-allow-unaligned-buffers.html

I have not set up coverage analysis for the fuzz tests. That would be interesting to see!

Cargo Klee sounds pretty useful too.

indo-dev-0 commented 4 years ago

With a few annotations sprinkled in, an automated prover should have no trouble checking whether those invariants hold.

Would mind annotating the existing codebase with these assertions, even if they were just debug asserts or code comments (i.e. Contracts, Adhesion, and/or Static Assertions)? I believe the work on safe transmutes would be of relevance here....

I have not set up coverage analysis for the fuzz tests. That would be interesting to see!

Fuzzcheck is the cool kid on the block.