search

SRI-CSL / OCCAM

OCCAM: Object Culling and Concretization for Assurance Maximization
BSD 3-Clause "New" or "Revised" License
26 stars 10 forks source link

Incorrect output with specialized binary using configuration priming: objdump, readelf #59

Closed mudbri closed 2 years ago

mudbri commented 2 years ago

The specialized binary of readelf and objdump, when specialized with configuration priming, result in an incorrect output. The files required to reproduce the problem can be found here. The issue can be reproduced in the following way:

  1. make
  2. make manifests
  3. For readelf: slash --work-dir=slash_readelf --enable-config-prime readelf.manifest followed by make test_readelf
  4. For objdump: slash --work-dir=slash_objdump --enable-config-prime objdump.manifest followed by make test_objdump

The test compares the output of the specialized binary against the output of the unspecialized binary using the same arguments and input file. The test fails when the --enable-config-prime flag is provided but passes when the flag is not provided (e.g. slash --work-dir=slash_objdump objdump.manifest). It seems like this issue is also caused by overspecialization.

caballa commented 2 years ago

I added a new option --config-prime-spec-only-globals (commit 8c49830) that when enabled reduces the likelihood of over-specialization. With this option, the specialized binary should produce the correct answer.

mudbri commented 2 years ago

Both of the applications are working correctly with the --config-prime-spec-only-globals option