Closed S1eGa closed 11 months ago
Happens on 32-bit compiled bc
1) Problem found in __uClibc_main
. KLEE allocates memory object argvMO, which includes in it argc
, argv
, envp
and auxv
(last one empty). If KLEE has been built on 64-bit machine, by default it uses malloc
, which gives 64-bit addresses. But it uses 32-bit version of uclibc for analysis. Therefore pointer to argv in code under analysis consists of only 4 bytes and can not be used to navigate through argvMO. It happens in the piece of code below from __uClibc_main.c:275
(memory error ariases from line while (*aux_dat) {
):
2) Another problem that KLEE uses 64-bit version of uClibc. On 32 and 64 bits machine sizes of unsigned long
differ. It leads to out-of-bound read in the same line as in point 1.
void __uClibc_main(int (*main)(int, char **, char **), int argc,
char **argv, void (*app_init)(void), void (*app_fini)(void),
void (*rtld_fini)(void), void *stack_end)
{
#ifndef __ARCH_HAS_NO_LDSO__
unsigned long *aux_dat;
ElfW(auxv_t) auxvt[AT_EGID + 1];
#endif
#ifndef SHARED
__libc_stack_end = stack_end;
#endif
__rtld_fini = rtld_fini;
/* The environment begins right after argv. */
__environ = &argv[argc + 1];
/* If the first thing after argv is the arguments
* the the environment is empty. */
if ((char *) __environ == *argv) {
/* Make __environ point to the NULL at argv[argc] */
__environ = &argv[argc];
}
#ifndef __ARCH_HAS_NO_LDSO__
memset(auxvt, 0x00, sizeof(auxvt));
aux_dat = (unsigned long*)__environ;
while (*aux_dat) {
aux_dat++;
}
// ...
// Some code
// ...
}
For now fast solution is to use flag --allocate-determ
to force KLEE return 32-bit addresses.
Solution of second point: build klee-libc with 32-bit support (this may be done by manual building of libc; we need to modify step make
-> make KLEE_CFLAGS="-m32"
). Additionally we need to make a shadow copy of errno
in 32-bit address space (not sure in this now?), which made in this branch.
Additionally we need to make a shadow copy of
errno
in 32-bit address space
It is required. Since function __errno_location
returns address, it size is equal to 4 on 32-bit machines. Therefore, dereferencing processes through this address and it requires existing memory object with this address.
Other way to handle it is to cut address for errno to 32 bit in every pointer resolution, but it seems less elegant solution.
With uClibc revealed significant regression on TestComp-benchmark: 1670 with uClibc vs. 2210 without uClibc. Also found many strange memory errors on coverage-error-call track.
From sv-benchmarks; run on
pals_STARTPALS_ActiveStandby.1.ufo.BOUNDED-10.pals.c
withlibc=uclibc
gives following log: