CVE-2014-3467: silently concretizing expression (reason: resolveOne failure)

[jordr]

The following applies to decoding.c:709 and decoding.c:1131 (and possibly the third vulnerability).

autoklee --exit-on-error-type=Ptr --libc=uclibc --posix-runtime --error-location=decoding.c:1131 --split-search --search=dfs --skip-functions-not=asn1_der_decoding,__fd_open,read,syscall,_asn1_yyparse,_asn1_yylex test.bc 32

gives the following warning and error: WARNING ONCE: silently concretizing (reason: resolveOne failure) expression and getLoadInfo() does not support symbolic addresses.

Full log below:

[6e6b35] KLEE: ■ ■ ■ ■ ■  __wrap_type_field175 (skipped)
[2875b3] KLEE: (((heuristics '__wrap_type_field175': 6/15/0.034707)))
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/15/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_extract_tag_der_recursive [1/6/1.471633]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/16/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/17/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/18/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆ ◆ ◆  __wrap__asn1_extract_tag_der [1/3/0.781942]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/19/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap_type_field175 [7/20/0.034707]
[af937e] KLEE: □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap__asn1_get_octet_string [1/7/3.220879]
[dc58bf] KLEE: ■ ■ ■ ■ ■  strtol
[dc58bf] KLEE: ■ ■ ■ ■ ■ ■  _stdlib_strto_l
[af937e] KLEE: □ □ □ □ □ □ □ ◆ ◆ ◆ ◆ ◆  __wrap__asn1_get_octet_string [1/8/3.313948]
[596f7d] KLEE: WARNING ONCE: silently concretizing (reason: resolveOne failure) expression (Add w64 94374332442432
          (Mul w64 2
                   (SExt w64 (SExt w32 (Extract w8 0 (Add w32 48
                                                              (SExt w32 (Extract w8 0 (SExt w64 (Add w32 3
                                                                                                         (Extract w32 0 (Select w64 (Slt 30
                                                                                                                                         (Add w32 1
                                                                                                                                                  N0:(ZExt w32 (Read w8 2 buf))))
                                                                                                                                    18446744073709551612
                                                                                                                                    (ZExt w64 N0))))))))))))) to value 94374332442536 (/home/ubuntu/code/klee-uclibc/libc/stdlib/stdlib.c:526)
	#000017912 in _stdlib_strto_l (str=94374335281880, endptr=0, base=10, sflag=1) at /home/ubuntu/code/klee-uclibc/libc/stdlib/stdlib.c:526
	#100017889 in strtol (str=94374335281880, endptr=0, base=10) at /home/ubuntu/code/klee-uclibc/libc/stdlib/stdlib.c:332
	#200006110 in asn1_der_decoding (element=94374337071824, ider=94374326325744, len=32, errorDescription=94374337068192) at /home/ubuntu/code/chopper-experiments/libtasn1/CVE-2014-3467/libtasn1-3.5//lib/decoding.c:1125
	#300012684 in run (buf_size=32) at /home/ubuntu/code/chopper-experiments/libtasn1/CVE-2014-3467/main.c:32
	#400012716 in __user_main (argc=2, argv=94374267265712, envp=94374267265736) at /home/ubuntu/code/chopper-experiments/libtasn1/CVE-2014-3467/main.c:44
	#500018317 in __uClibc_main (main=94374263606304, argc=2, argv=94374267265712, app_init=0, app_fini=0, rtld_fini=0, stack_end=0) at /home/ubuntu/code/klee-uclibc/libc/misc/internals/__uClibc_main.c:401
	#600020349 in main (=2, =94374267265712)
getLoadInfo() does not support symbolic addresses
UNREACHABLE executed at /home/jruiz/code/chopper/lib/Core/Executor.cpp:4387!

Note: this follows a

[d6c361] KLEE: ERROR: /home/ubuntu/code/chopper-experiments/libtasn1/CVE-2014-3467/libtasn1-3.5//lib/parser_aux.c:233: concretized symbolic size

shortly before

[jordr]

libtasn1 bench: reach the ptrerror on each CVE