Error when analyze shared library

[Mengyuan-L]

Hi, I met a problem when I try to use wp to analyze some shared libraries. The command looks like:
bap wp --func=XXXXX --show=refuted-goals --postcond=" (assert (= RAX #x0000000000000002)) " ./libcrypto.so.3
The output looks like:

\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \n")
\n")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "lib/wp_utils.ml", line 70, characters 18-50
Called from file "lib/wp_analysis.ml", line 27, characters 6-92
Called from file "src/list.ml", line 387, characters 13-17
Called from file "src/list.ml" (inlined), line 418, characters 15-31
Called from file "lib/wp_analysis.ml", line 38, characters 19-45
Called from file "wp.ml", line 374, characters 2-32
Called from file "cmdliner_term.ml", line 25, characters 19-24
Called from file "cmdliner_term.ml", line 23, characters 12-19
Called from file "cmdliner.ml", line 117, characters 32-39
Called from file "cmdliner.ml", line 147, characters 18-36
Called from file "cmdliner.ml", line 265, characters 22-48
Called from file "lib/bap_main/bap_main.ml", line 1105, characters 10-99
Called from file "lib/bap_main/bap_main.ml", line 1279, characters 15-140
Called from file "src/bap_frontend.ml", line 320, characters 8-127

I use the docker image directly and wp can work pretty well for some small binaries. Since the problem is a little bit similar to BAP #1086
so I try to have bap 2.2.0 installed. After pinning the bap version to 2.2.0, I met the following error:

am/4.09/lib/z3 -I /home/opam/.opam/4.09/lib/zarith -I /home/opam/.opam/4.09/lib/zip -no-alias-deps -open Bap_wp -o src/.bap_wp.objs/byte/bap_wp__Environment.cmi -c -intf src/environment.pp.mli)
File "src/environment.mli", line 129, characters 29-42:
129 | -> specs:(Bap.Std.Sub.t -> Theory.target -> fun_spec option) list
^^^^^^^^^^^^^
Error: Unbound type constructor Theory.target
Makefile:38: recipe for target '_build/install/default/lib/bap_wp/bap_wp.cmxa' failed
make[1]: Leaving directory '/home/opam/cbat_tools/wp/lib/bap_wp'
make[1]: *** [_build/install/default/lib/bap_wp/bap_wp.cmxa] Error 1
make: *** [install.lib] Error 2
Makefile:75: recipe for target 'install.lib' failed

Do you have any suggestions or comments? Thanks in advance.

[codyroux]

Can you give the specific version of bap, say the output of bap --version?

Thanks

[Mengyuan-L]

Can you give the specific version of bap, say the output of bap --version?

Thanks

The bap version in the docker is
2.4.0-alpha+ea79178

I also tried to change the Dockerfile
FROM binaryanalysisplatform/bap:latest
to
FROM binaryanalysisplatform/bap:2.1.0

Then I met the same error as when I pinned bap to 2.2.0

Error: Unbound type constructor Theory.target

[codyroux]

Hi, pinning to older versions of BAP won't help, since WP is supposed to work on a recent version.

Not sure what is causing your error though. Is there any chance you can help us reproduce it?

Ideally we'd need the inputs you used, or barring that the full stacktrace.

[codyroux]

Now that I mention this, it would be nice to know what the toplevel error is (i.e. the first line of the error).

[Mengyuan-L]

Now that I mention this, it would be nice to know what the toplevel error is (i.e. the first line of the error).

Thanks for your help.
This is the command I use
bap wp --func=BN_clear_bit --show=refuted-goals --postcond=" (assert (= RAX #x0000000000000002)) " ./libcrypto.so.3

The binary libcrypto.so.3 is under /usr/local/lib/ . I have tried two versions of libcrypto and both faced the same error. You may try your libcrypto and I also upload my version to google drive just in case. Here is the link for my libcrypto: LIBCRYPTO

and here is the toplevel error

opam@7cd28966a5fc:~/cbat_tools/wp$ bap wp --func=BN_clear_bit --show=refuted-goals --postcond=" (assert (= RAX #x0000000000000002)) " ./libcrypto.so.3
Uncaught exception:
(Failure
"Error loading project: (("Stack overflow")
\n "Raised by primitive operation at file \"z.ml\", line 148, characters 7-19\
\n \nCalled from file \"lib/bap_types/bap_bitvector.ml\" (inlined), line 65, characters 31-51\
\n \nCalled from file \"lib/bap_types/bap_bitvector.ml\" (inlined), line 67, characters 17-23\
\n \nCalled from file \"lib/bap_types/bap_bitvector.ml\" (inlined), line 154, characters 17-34\
\n \nCalled from file \"lib/bap_types/bap_bitvector.ml\", line 621, characters 42-54\
\n \nCalled from file \"lib/bap_types/bap_bil.ml\", line 66, characters 23-26\
\n \nCalled from file \"src/list.ml\", line 1085, characters 12-19\
\n \nCalled from file \"lib/bap_types/bap_stmt.ml\", line 198, characters 13-28\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 630, characters 28-37\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 604, characters 10-19\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1763, characters 12-33\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\" (inlined), line 1529, characters 4-16\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1540, characters 34-51\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1583, characters 53-56\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1264, characters 6-23\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1839, characters 29-226\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\" (inlined), line 1847, characters 13-36\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 2141, characters 25-50\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1763, characters 12-33\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\" (inlined), line 1529, characters 4-16\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1549, characters 38-55\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1583, characters 53-56\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1570, characters 60-63\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 1783, characters 25-112\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 2435, characters 30-65\
\n \nCalled from file \"src/map.ml\", line 747, characters 21-31\
\n \nCalled from file \"src/map.ml\", line 754, characters 26-45\
\n \nCalled from file \"src/map.ml\", line 754, characters 26-45\
\n \nCalled from file \"src/map.ml\", line 754, characters 26-45\
\n \nCalled from file \"src/map.ml\", line 754, characters 26-45\
\n \nCalled from file \"src/map.ml\", line 754, characters 26-45\
...
\n \nCalled from file \"src/map.ml\", line 1677, characters 11-85\
\n \nCalled from file \"lib/knowledge/bap_knowledge.ml\", line 2433, characters 29-274\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 60-63\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29
...
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \nCalled from file \"lib/monads/monads_monad.ml\" (inlined), line 1029, characters 29-34\
\n \nCalled from file \"lib/monads/monads_monad.ml\", line 1034, characters 38-42\
\n \n")
\n")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "lib/wp_utils.ml", line 70, characters 18-50
Called from file "lib/wp_analysis.ml", line 27, characters 6-92
Called from file "src/list.ml", line 387, characters 13-17
Called from file "src/list.ml" (inlined), line 418, characters 15-31
Called from file "lib/wp_analysis.ml", line 38, characters 19-45
Called from file "wp.ml", line 374, characters 2-32
Called from file "cmdliner_term.ml", line 25, characters 19-24
Called from file "cmdliner_term.ml", line 23, characters 12-19
Called from file "cmdliner.ml", line 117, characters 32-39
Called from file "cmdliner.ml", line 147, characters 18-36
Called from file "cmdliner.ml", line 265, characters 22-48
Called from file "lib/bap_main/bap_main.ml", line 1105, characters 10-99
Called from file "lib/bap_main/bap_main.ml", line 1279, characters 15-140
Called from file "src/bap_frontend.ml", line 320, characters 8-127

Thanks again for your help

[codyroux]

Aha. The error here is a BAP one, I think: it is failing to load the project, because the disassembly is taking too much stack space.

My understanding is that crypto code is inherently computationally hard to uplift.

One "easy" solution would be to raise the stack space, e.g.

ulimit -s unlimited

and try again. Warning: this will likely use large amounts of your live memory.

Another, more experimental route would be to use the "raw" loader for BAP with some options which limit the amount of disassembled code, to include only the function of interest (see here).

This is probably a bit finicky though.

A final bit of pessimism: currently, I'm not sure CBAT will handle large crypto subroutines in any reasonable time. We probably need some special optimizations to break the problem into smaller pieces.