4 ms·
> Just remember to aid others' verification efforts later on by keeping it modular, minimal shared state, simple constructions in code, and so on. Whatever pass
by zx2c4 10y ago
> Just remember to aid others' verification efforts later on by keeping it modular, minimal shared state, simple constructions in code, and so on. Whatever passes through a decent static analysis tool.
Yes this absolutely is the goal. I'm trying to keep the codebase as small and clear as possible.
> Design by Contract
Working out the precise pre and post conditions of every state would indeed be worthwhile. For all state transitions of the protocol, I've worked out by hand every possible combination and accounted it for it. I should publicize this work (i.e. type up my handwritten notes), and then let others join building on top of it.
- nickpsecurity 10y ago"Working out the precise pre and post conditions of every state would indeed be worthwhile. For all state transitions of the protocol, I've worked out by hand every possible combination and accounted it for it. I should publicize this work (i.e. type up my handwritten notes), and then let others join building on top of it." That's actually... great. It's exactly what high-assurance security did in kernels and VPN's. I'm impressed. You should definitely write that up and share it for peer review. Also, since you've done it, the next step is to review each one to make sure security properties are maintained or it fails fast, safe, and loud. :)