Unable to run binsec-rel with XMSS due to `_enum limit reached_`

[JoaoDiogoDuarte]

Hi!

I am trying to run binsec-rel on a reference XMSS implementation and I'd just like to report that I cannot seem to do so.

I have made a fork of the XMSS implementation here: https://github.com/JoaoDDuarte/xmss-reference-binsec-rel

As far as I know, I labelled all the high and low inputs correctly and binsec-rel installed successfully. I also specified the esp pointer in the memory.txt. I also built the binary with these inputs with the static flag.

When I run binsec -relse xmss_binsec, I get the following output:

[relse:warning] No entrypoint: starting from main.
[relse:warning] [Stub] Symbol bzero not found
[relse:warning] Found as many solutions for
                (concat (select __memory_0 (_ bv139325495 32))
                (concat (select __memory_0 (_ bv139325494 32))
                (concat (select __memory_0 (_ bv139325493 32))
                (select __memory_0 (_ bv139325492 32))))) as asked.
                Possibly incomplete solution set.
[relse:warning] Dynamic jump (08049078, 0) : goto @[0x084df034,4] 
                could have led to invalid address {0x41028105; 32}; skipping
[relse:warning] Dynamic jump (08049078, 0) : goto @[0x084df034,4] 
                could have led to invalid address {0x01010101; 32}; skipping
[relse:warning] Dynamic jump (08049078, 0) : goto @[0x084df034,4] 
                could have led to invalid address {0x00000000; 32}; skipping
[relse:result] [Exploration] End of the RelSE
[relse:info] RelSE stats:
                           Total queries: 
                                            SAT:        1
                                            UNSAT:      0
                                            Other:      0
                                            Total:      1
                                            Time:       0.021774
                                            Time avg:   0.021774
                           Exploration queries: 
                                                  SAT:  1
                                                  UNSAT:        0
                                                  Other:        0
                                                  Total:        1
                                                  Time: 0.021774
                                                  Time avg:     0.021774
                           CF Insecurity queries: 
                                                    SAT:        0
                                                    UNSAT:      0
                                                    Other:      0
                                                    Total:      0
                                                    Time:       0.000000
                                                    Time avg:   -nan
                           Mem Insecurity queries: 
                                                     SAT:       0
                                                     UNSAT:     0
                                                     Other:     0
                                                     Total:     0
                                                     Time:      0.000000
                                                     Time avg:  -nan
                           Term Insecurity queries: 
                                                      SAT:      0
                                                      UNSAT:    0
                                                      Other:    0
                                                      Total:    0
                                                      Time:     0.000000
                                                      Time avg: -nan
                           Insecurity queries: 
                                                 SAT:   0
                                                 UNSAT: 0
                                                 Other: 0
                                                 Total: 0
                                                 Time:  0.000000
                                                 Time avg:      -nan
                           Model queries: 
                                            SAT:        0
                                            UNSAT:      0
                                            Other:      0
                                            Total:      0
                                            Time:       0.000000
                                            Time avg:   -nan
                           Enum queries: 
                                           SAT: 0
                                           UNSAT:       0
                                           Other:       0
                                           Total:       0
                                           Time:        0.000000
                                           Time avg:    -nan
                           Total queries: 
                                            SAT:        1
                                            UNSAT:      0
                                            Other:      0
                                            Total:      1
                                            Time:       0.021774
                                            Time avg:   0.021774
                           Query size avg/max:  359.000000 / 359
                           Checks done/spared:  0 / 28
                           Coverage: 
                                       Paths:           0
                                       Conditionals:    0
                                       Forks:   0
                                       DBA Instructions:        126
                                       x86 Instructions:        34
                           Violations:          0
                           Status:      _enum limit reached_
                           Result:      Unknown
                           Elapsed time:        0.246062

I am not certain why this is happening as I am relatively new to the tool, but it seems as if the inputs are currently too large for binsec-rel to handle. Is my intuition correct, please? Also, do you know if there is some way to increase the enum limit?

Thanks! João

[Lesly-Ann]

Enumerations usually happen when there is an indirect jump. Is 0x08049078 a ret instruction?

Basically, Binsec tries to enumerate jump targets and it seems that in your case the jump target is symbolic (and not well defined), meaning that the indirect jump can have an arbitrary target.

[JoaoDiogoDuarte]

Thanks for the fast reply!

So the instruction 0x08049078 is a jmp instruction to 0x84df034:

8049078:    ff 25 34 f0 4d 08       jmp    *0x84df034

whereby 0x84df034 is not mentioned anywhere else in the assembly code so I am not sure what address is inside 0x84df034, which explains the output of binsec-rel.

Does this mean that I need to find a new implementation of XMSS or is there any way of circumventing this by any chance?

[Lesly-Ann]

If you know where the jump should go you can provide a DBA stub to replace the jump / or initialize the memory at address 0x84df034 with the correct location.

[JoaoDiogoDuarte]

So I figured out that the issue came from a switch statement which (in my case) will always result in the same value, so I just removed it.

However, I now get the error:

[relse:warning] No entrypoint: starting from main.
[relse:warning] [Stub] Symbol bzero not found
Fatal error: exception Failure("not_yet_implemented: instruction #unsupported 0f 11 06 at address 0804a4f3")

And the instruction is:

 804a4f3:   0f 11 06                movups %xmm0,(%esi)

I am guessing this is a dead end as this would require expanding binsec-rel? I would volunteer but I know nothing of OCaml...

[JoaoDiogoDuarte]

This seems to be solved if I compile with the -mno-sse, so I will do this for now and fix some more dynamic jumps :) If I run into anything else, I will let you know!

Thanks

[Lesly-Ann]

Unfortunately, Binsec does not support floating point instructions and SSE. But if you can disable SSE it should be good :)

[Lesly-Ann]

(And adding support for this would probably be a lot of work, even if you know OCaml ^^)

[JoaoDiogoDuarte]

Makes sense! I managed to get rid of the other annoying dynamic jumps by passing -O1 instead of -03` - issue is is that binsec says:

Fatal error: exception Failure("not_yet_implemented: instruction @assert ((ebx<32> != 0<32>)) at address 0804a27b")

The address isn't in my assembly... I think I've spent too long looking at pointers, this is work for tomorrow me :)

[Lesly-Ann]

I guess your control-flow is going wild at some point. You can try to track where that happens by looking at the addresses of executed instructions. I would suggest to look at the debug trace and make sure that return instructions jump to the right target.

Good luck for tomorrow :muscle:

[JoaoDiogoDuarte]

Ok, I guess I looked at it a little earlier, the issue is that binsec says

[relse:warning] No entrypoint: starting from main.
[relse:warning] [Stub] Symbol bzero not found
Fatal error: exception Failure("not_yet_implemented: instruction @assert ((esi<32> != 0<32>)) at address 08049bea")

and the instruction is

 8049bea:   f7 f6                   div    %esi

Do you have any advice on tackling this? If not, I'll just close the issue as it seems to be more worthwhile to find another implementation :)