Comments (7)
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.)
from capnproto-rust.
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.
from capnproto-rust.
@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.
from capnproto-rust.
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
from capnproto-rust.
@dwrensha what is the code coverage on the fuzz tests?
from capnproto-rust.
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.
from capnproto-rust.
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.
from capnproto-rust.
Related Issues (20)
- Primitive list panicks if the list type is `Void` HOT 1
- Null values for non active union members HOT 3
- Switch Allocator to act more like an owned arena HOT 8
- Reader fails with out of bounds pointer error when reading from compressed stream HOT 1
- Revert text setter ergonomics pessification; add raw_set methods HOT 6
- calculator example fails with java server: Cannot read capability pointer without capTable HOT 2
- c++.capnp compiles to unusable module name HOT 6
- How to send generated readers across threads HOT 3
- From bytes to TypedReader HOT 6
- Allowing construction of NoAllocSliceSegments with buffer and NoAllocBufferSegmentType HOT 7
- Kudos to builders of this Rust library - Every single one of you. HOT 3
- [Question]How to extract generic type values HOT 5
- capnp_rpc does not work on monoio HOT 4
- Dynamic parsing of fields may panic HOT 1
- traits.ListIter incorrectly implementing ExactSizeIterator HOT 1
- oc
- Using same schema file for both Rust and C++ HOT 1
- doc: read_message_from_flat_slice_no_alloc docstring bad autocomplete HOT 1
- Making rust capn proto fully async HOT 2
- Is there any reason why Rc<RefCell> is used compared to Arc<Mutex>?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from capnproto-rust.