Binary Tool Verification
The table below shows an overview of all 9 bugs we have found in other tools and semantics, during our work on libLISA. It includes 6 distinct bugs first listed in our 2024 paper, where we verified the correctness of Dasgupta et al.'s semantics implemented in the K framework. It also includes one bug in Bochs we found during development of Sem86, and several others found during the development of libLISA.
Insufficient cache invalidation causes incorrect page faults
Bochs uses an instruction cache to speed up instruction execution. This instruction cache needs to be cleared whenever the contents in memory change, or if the page table is updated.
One particular edge-case is instructions that cross page bounds.
For example, a 3-byte instruction at 0x1fff covers both page 0x1___ and 0x2___.
When the page 0x2___ was unmapped, the cache entry for the instruction at 0x1fff failed to be invalidated.
This caused Bochs to trigger page faults too late: instead of a page fault at 0x2000 when the instruction at 0x1fff was executed, a page fault at 0x2002 would occur when the following instruction was executed.
XCHGL is disassembled incorrectly
The instruction XCHGL EAX, EAX can be encoded as both 87C0 and 90. The second encoding has the semantics of NOP (do nothing), while the first has the semantics of XCHGL (set the upper 32 bits of RAX to zero). objdump, the disassembler used by Dasgupta et al. incorrectly disassembles 90 with a REX prefix as XCHGL instead of NOP."
This bug has since been fixed in binutils. Please note that older versions of Ubuntu ship old versions of binutils that still contain this bug. You will need a version newer than Ubuntu 22.04.
ARM64 executes wrong instruction when pc=0xFFFFFFFFFFFFFFFC
When an instruction was placed and executed at the highest possible address, 0xFFFFFFFFFFFFFFFC, and then unmapped, it wasn't properly removed from caches.
When later placing a new instruction at 0xFFFFFFFFFFFFFFFC and executing it, the old instruction would be executed instead.
RISC-V64 errors when calling emu_start with count = 1 at end of page
When executing a single instruction at the end of a page with the following page unmapped, unicorn would return a memory error (FETCH_UNMAPPED) instead of stopping.
This was caused by Unicorn decoding the next instruction, before checking if it should interrupt execution.
Because of this, a fetch to the unmapped page would always occur after executing the single instruction,
causing an error to be returned.
Incorrect bit offset for BT/BTS/BTR/BTC with memory operand
In all bit test variants (BT/BTS/BTR/BTC) on memory with a register bit offset, the bit offset is computed incorrectly. The bit offset is converted to a byte offset by shifting right by 3, then zero-extending the result to 64 bits. It should be sign-extended, to preserve the sign bits of negative offsets.
CMPS performs comparison incorrectly
The CMPS variants perform a comparison by setting flags according to Mem2 - Mem1, but they should be set according to Mem1 - Mem2.
OF incorrect for RCLB/RCRB
The overflow flag (OF) of RCLB/RCRB is undefined when the masked rotate count is not 0 or 1. However, Dasgupta et al. specifies the OF as undefined when the masked rotate count modulo the operand size + 1 is not 0 or 1.
vmpsadbw_xmm_xmm_m128_imm8 writes to wrong destination
The VMPSADBW instruction incorrectly writes to the source operand (R3) instead of destination operand (R4).
Crash when MULX is executed with identical destination registers
The MULX instructions write a result to two destination operands. The destination operands can be equal. Dasgupta et al.'s semantics have not taken this possibility into account, causing the K prover to crash when MULX with equal destination operands is executed.