undefined symbol: Z3_mk_seq_concat

[celestial-d]

I am using the image from http://panda-re.mit.edu/qcows/linux/ubuntu/1804/x86_64/bionic-server-cloudimg-amd64-noaslr-nokaslr.qcow2 and attempt to use the file_taint on a simple example of just cating a file. What I get is the following output (undefined symbol: Z3_mk_seq_concat)

./panda/build/x86_64-softmmu/panda-system-x86_64 -m 4096 /home/duo/Downloads/bionic-server-cloudimg-amd64-noaslr-nokaslr.qcow2 -replay cat_test -panda file_taint:filename=/root/osi_linux/kernelinfo.conf -panda osi -os linux-64-ubuntu:my_info PANDA[file_taint]:adding argument filename=/root/osi_linux/kernelinfo.conf. PANDA[core]:os_familyno=2 bits=64 os_details=ubuntu:my_info PANDA[core]:initializing file_taint PANDA[core]:loading required plugin syscalls2 PANDA[core]:initializing syscalls2 PANDA[syscalls2]:using profile for linux x64 64-bit PANDA[core]:loading required plugin hooks PANDA[core]:initializing hooks PANDA[core]:loading required plugin osi PANDA[core]:initializing osi PANDA[core]:loading required plugin osi_linux PANDA[core]:initializing osi_linux PANDA[osi_linux]:W> failed to read task.switch_task_hook_addr PANDA[osi_linux]:W> kernelinfo bytes [20-23] not read PANDA[core]:loading required plugin syscalls2 PANDA[core]:/home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_syscalls2.so already loaded PANDA[core]:loading required plugin taint2 Failed to load /home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_taint2.so: /home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_taint2.so: undefined symbol: Z3_mk_seq_concat PANDA[core]:FAILED to load required plugin taint2 from /home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_taint2.so Aborted (core dumped)

Before I run the experiment, I installed panda through the script install_ubuntu.sh. Also, I added the configure info (ubuntu:my_info:64) to the kernelinfo.conf based on your README in osi_linux

The version is r-18-06-3449-g81b0e25b11

[AndrewFasano]

What is your host OS and version?

Can you paste the output from running ldd /home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_taint2.so?

Have you installed the package libz3-dev? Do you have a file like /lib/x86_64-linux-gnu/libz3.so.*?

I'm not sure what version number you have there - are you using the dev branch of PANDA?

[celestial-d]

My system is Ubuntu 18.04.2 LTS with kernel 5.4.0-77-generic and I am not sure what branch of PANDA I use. I use 'git describe --tag' to check the version and the result shows r-18-06-3449-g81b0e25b11. After download the panda (git clone https://github.com/panda-re/panda.git), I copy the install_ubuntu.sh to panda_tmp folder and run it. I do not run any git operations to change a branch.

For libz3-dev, i see the default version z3 through 'sudo apt-get install libz3-dev' is 4.4, which cannot be used to compile PANDA. Thus I downloaded the source code of z3 (version 4.8.11, https://opam.ocaml.org/packages/z3/z3.4.8.11/), compiled and installed. After that, I run the install_ubuntu.sh.

I lists the output result of ldd below: $ ldd /home/duo/qemu/panda_tmp/panda/build/x86_64-softmmu/panda/plugins/panda_taint2.so linux-vdso.so.1 (0x00007ffcebecd000) libLLVM-11.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-11.so.1 (0x00007fee7a4ff000) libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fee7a2fb000) libz3.so.4 => /usr/lib/x86_64-linux-gnu/libz3.so.4 (0x00007fee790ea000) libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fee78d61000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fee78b49000) libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fee7892a000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fee78539000) /lib64/ld-linux-x86-64.so.2 (0x00007fee7f71d000) libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fee78331000) libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fee780fa000) libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fee77edd000) librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fee77cd5000) libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fee77aab000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fee7770d000) libxml2.so.2 => /usr/lib/x86_64-linux-gnu/libxml2.so.2 (0x00007fee7734c000) libgomp.so.1 => /usr/lib/x86_64-linux-gnu/libgomp.so.1 (0x00007fee7711d000) libicuuc.so.60 => /usr/lib/x86_64-linux-gnu/libicuuc.so.60 (0x00007fee76d65000) liblzma.so.5 => /lib/x86_64-linux-gnu/liblzma.so.5 (0x00007fee76b3f000) libicudata.so.60 => /usr/lib/x86_64-linux-gnu/libicudata.so.60 (0x00007fee74f96000)

[AndrewFasano]

'sudo apt-get install libz3-dev' is 4.4, which cannot be used to compile PANDA.

Why can't you use that version to build PANDA? Perhaps the fact that you built from source is making something strange go on with the loader - maybe you could try running sudo ldconfig. Not positive if that would help given that ldd is correctly finding the library.

If that doesn't help, what's the output from readelf -a /usr/lib/x86_64-linux-gnu/libz3.so.4 | grep Z3_mk_seq_concat

If your libz3 is set up correctly, you should see something like

   357: 0000000001260ac0   245 FUNC    GLOBAL DEFAULT   14 Z3_mk_seq_concat

[celestial-d]

If I use the z3 (version 4.4.1), the panda will have compiling problem. I see you answered the question before (https://github.com/panda-re/panda/issues/1015). It seems that my libz3 does not set up correctly. When I run the command sudo ldconfig or readelf, there is nothing in the output. Could you provide a available z3 package link?

[AndrewFasano]

I'm running Ubuntu 20.04 and the version of libz3-dev from apt works fine with panda - In issue #1015 we were discussing the version of libz3-dev available in Ubuntu 18.04 apt so you shouldn't have to worry about building from source since you're on 20.04.

$ apt info libz3-dev
Package: libz3-dev
Version: 4.8.7-4build1
Priority: extra
Section: universe/libdevel
Source: z3
Origin: Ubuntu
Maintainer: Ubuntu Developers <ubuntu-devel-discuss@lists.ubuntu.com>
Original-Maintainer: LLVM Packaging Team <pkg-llvm-team@lists.alioth.debian.org>
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 521 kB
Depends: libz3-4 (= 4.8.7-4build1)
Homepage: https://github.com/Z3Prover/z3
Download-Size: 67.5 kB
APT-Manual-Installed: yes
APT-Sources: http://mirrors.mit.edu/ubuntu focal/universe amd64 Packages
Description: theorem prover from Microsoft Research - development files
 Z3 is a state-of-the art theorem prover from Microsoft Research. It can be
 used to check the satisfiability of logical formulas over one or more
 theories. Z3 offers a compelling match for software analysis and verification
 tools, since several common software constructs map directly into supported
 theories.
 .
 This package can be used to invoke Z3 via its C++ API.

Here's a simple pypanda tests I just ran that passed for me:

from pandare import Panda
panda = Panda(generic="i386")

success = False

@panda.queue_blocking
def driver():
    panda.record_cmd("cat /etc/passwd | wc -l", recording_name="filetaint")
    panda.stop_run()
panda.run() # take recording

@panda.ppp("taint2", "on_taint_change")
def taint_change(*args):
    print("Taint changed!")
    global success
    success = True
    panda.end_analysis()

panda.load_plugin("file_taint", {"filename": "/etc/passwd"})
panda.run_replay("filetaint")

assert(success)

[celestial-d]

Sorry, my system is ubuntu 18.04.2 LTS, not 20.04, thus I need to consider the version problem.

[buszk]

@AndrewFasano My bad here. I encountered this too while building panda in Ubuntu 18. The default libz3-dev package for ubuntu 18 is just too old. I will open a PR that removes it from Ubuntu 18 dependencies and compile/install a custom version in build script.

@celestial-d Can you do sudo apt remove libz3-dev and install z3 version 4.8.7 from https://github.com/Z3Prover/z3/releases

[celestial-d]

@buszk I compiled with z3 version 4.8.7 successfully, but running the file-taint plugin meets an error after compilation.

[buszk]

You may try sudo apt remove libz3-dev and recompile panda

You can use ldd to figure out what libz3.so is dynamically linked to the so file that failed to load. It might still be linked to the old z3 package you have. In this case, removing the package can solve the problem.

[AndrewFasano]

This should be resolved thanks to @buszk's PR #1064. Feel free to reopen if you still experience this issue.