5 ms·
I don't think it matters because hacspec on this case is just the language which is a subset of rust. He still just uses cargo so treat it as rust code. The po
by dudus 3y ago
I don't think it matters because hacspec on this case is just the language which is a subset of rust. He still just uses cargo so treat it as rust code.
The point is that you can check the binary against some sort of formal definition to make sure the implementation you have at hand has not been tampered with. But it seems the idea is to check during dev not usage which for me is a missed opportunity. Why can't it check if it's correct every time it's loaded?
Keep in mind that Bertie is written in hacspec -- a more "restrictive" version of Rust that lends itself to formal verification. Working on Bertie feels a lot like working on a typical Rust crate but all code needs to be valid according to hacspec. Thus, you may also find that some code is "unusual" compared to vanilla Rust.
- nickpsecurity 3y agoSounds like SPARK Ada and Frama-C.
- tialaramex 3y ago> Why can't it check if it's correct every time it's loaded? This is considerable extra work and it's pointless. When you add together some numbers do you find yourself having to painstakingly re-assess whether the Peano Axioms (which make arithmetic work) do what you expected for the numbers you're adding? But what if today, this time, 2 + 2 is 7 or 5 instead of 4?
- dudus 3y agoI do find myself painstakingly repeating tests after every commit no matter how minor it is.
- rfl890 3y agoAt runtime you could simply verify the dll‘s signature or any other generic code integrity solution? Why go to all the trouble to verify your implementation at runtime when you could do it at compile time?