Fix segfaults in mm0-c implementations

[melg8]

I found two different segfaults in mm0-c implementation using afl-fuzz/klee.

Here i add two files which can be used to reproduce problem in original source code and fixes to this problems.

To reproduce on original source code:

1. Revert commits with "fix" in commit message.
2. cd mm0-c
3. ./make.sh

./a.out ../tests/mmb/run/gi_header_p_index_overflow.mmb < ../examples/tutorial/02-mm0-intro.mm0  

./a.out ../examples/tutorial/03-mm1-intro.mmb < ../tests/mm0_mmu/run/binders_overflow_in_axiom.mm0 

Related

I have a question, could this problems be found with formal verification? if yes - maybe this defects in original source code could be used to verify, that indeed formal verification could find them.

I didn't check other implementations of verifiers - maybe they have similar problem.
I found some of mmb files could hang verifier for 8-10 second on my machine - if you interested, i can share them.

Additionally: I'm really new to formal verification stuff, but if you give me 2 examples of mm0 files which couldn't (should never) be proved by any mmb file (one example should be 10-20 lines) and second big and complex. Than i could fuzz them too.

Is there any chat/discord/iirc where i can ask some questions about mm0 and in general about verification topic?

[ammkrn]

I didn't check other implementations of verifiers - maybe they have similar problem.

The rust parser catches both of these and returns suitable error messages before any attempt at verification begins. 03-mm1-intro.mmb, has a bad index, and gi_header_p_index_overflow.mmb has a properly formed header, but one that indicates there's something wrong with the file as a whole.

The mm1 parser and mmb parser both have cargo fuzz set up and contain some basic tests if you're interested in fuzzing the rust components.

[digama0]

Thanks for the PR and fuzzing! As Knuth would say, I have not tested the code, only proved it correct. :)

The binder issue is a bug, but the fix isn't quite right. The ALLOC macro is supposed to always return an inbounds pointer, so it's not necessarily an issue that we are dereferencing it directly, but it hits the -1 sentinel value which is supposed to be impossible for theorems. I've added a check that theorems should end in a statement.

For the second issue, it's actually likely to be a recurring issue, since after double checking the spec it looks like even forming pointers out of bounds of an allocation is UB on a strict reading of the standard. That is, I often do pointer checks like assert(&p[attacker_value] < end); *p and the C spec says that if the computation of p + attacker_value overflows or goes past end then it is already UB even before the dereference. If one assumes that the compiler respects wraparound arithmetic here, then assert(p <= &p[attacker_value] < end); is sufficient, but the recommendation appears to be to do integer checks like attacker_value < end - p instead. Well... this is why I don't like C.

I have a question, could this problems be found with formal verification? if yes - maybe this defects in original source code could be used to verify, that indeed formal verification could find them.

Yes indeed, that's the plan. It's a rather long term plan though - I'm currently working on the compiler that will eventually be able to verify programs written in a new language, into which mm0-c will be rewritten. This C version will continue to stick around, so bugfixes like this are always appreciated.

I found some of mmb files could hang verifier for 8-10 second on my machine - if you interested, i can share them.

Oh, that's quite interesting indeed. I assume this isn't merely a gigantic file? Taking into account the architectural limitations of mm0-c that mean that large files should just fail with a resource exhaustion error, it shouldn't be possible to make the verifier take a long time unless you use a large file.

Additionally: I'm really new to formal verification stuff, but if you give me 2 examples of mm0 files which couldn't (should never) be proved by any mmb file (one example should be 10-20 lines) and second big and complex. Than i could fuzz them too.

I'll come up with something for this tomorrow.

Is there any chat/discord/iirc where i can ask some questions about mm0 and in general about verification topic?

You can post issues here, but there isn't a dedicated chat platform for mm0. I often hang out on https://leanprover.zulipchat.com so you can ping me there if you want to chat. Maybe I could create an opt-in stream there for MM0, if there is interest...

[digama0]

@melg8

Additionally: I'm really new to formal verification stuff, but if you give me 2 examples of mm0 files which couldn't (should never) be proved by any mmb file (one example should be 10-20 lines) and second big and complex. Than i could fuzz them too.

I've added miu.mm0 as a simple but interesting example of an unprovable theorem, and unprovable.mm0 as an even simpler example. As for complex examples, I can't do much better than verifier_join.mm0 (you have to concatenate the files included by verifier.mm0 for mm0-c to accept it; mm0-rs has a tool to do this via mm0-rs join verifier.mm0 > verifier_join.mm0).

[melg8]

@digama0 thanks! i'll check it out