Infinite loop while scanning a gadget

[andyhhp]

I've found one gadget which seems to never terminate when scanned. This behaviour is repeatable:

$ ./inspectre analyze /local/xen.git/xen/xen-syms --address-list addr-list-parse_event_log_entry.csv --base 0xffff82d040200000 --config config_all.yaml --output out/gadgets.csv --asm out/asm
[MAIN]  Loading angr project...
[MAIN]  Removing non-writable memory...
[MAIN]  Analyzing gadget at address 0xffff82d040209729 parse_event_log_entry ...

^C

Files: xen-syms.gz addr-list-parse_event_log_entry.csv

The source for this function is https://github.com/xen-project/xen/blob/9659b2a6d73b14620e187f9c626a09323853c459/xen/drivers/passthrough/amd/iommu_init.c#L533

The disassembly with annotated jumps is: parse_event_log_entry.disassembly.txt

There's only one backwards jump at all, and it's a simple loop at https://github.com/xen-project/xen/blob/9659b2a6d73b14620e187f9c626a09323853c459/xen/drivers/passthrough/amd/iommu_init.c#L583

[SanWieb]

Thanks again,

I looked quickly at it and it seems that the function vprintk_common (called by ffff82d04020987d > printk) produces high/infinite number of states. Not sure if we can avoid this, we will have a look. (@AlviseDeFaveri the state is splitted many times on the pushfq instruction in vprintk_common)

If we run multiple targets we always use the run-parallel script. It is faster since parallelization in Python script is a mess, and we set a timeout for each gadget to cover these infinite loops. So I would recommend to use that script also.

[AlviseDeFaveri]

Thanks for the detailed report, will look into it

[andyhhp]

Ah - I'd found Z3Timeout in the config file and assumed this applied to the whole analysis. I'm giving the parallel script a try right now

[AlviseDeFaveri]

Seems to be fixed in new version, please reopen if this is not the case

➜ time ../../inspectre analyze xen-syms --config config_all.yaml --base 0xffff82d040200000 --address 0xffff82d040209729 --output out/gadgets.csv --asm out/asm
[MAIN]  Loading angr project...
[MAIN]  Removing non-writable memory...
[MAIN]  Analyzing gadget at address 0xffff82d040209729...
[MAIN]  Found 1 potential transmissions.
[MAIN]  Found 0 tainted function pointers.
[MAIN]  Extracted 1 transmissions.
[MAIN]  --------------- ANALYZING TRANSMISSIONS ------------------
[MAIN]  Analyzing <BV64 0xffff82d0403f9360 + (0#29 .. 0x7fffffff8 + ((0#31 .. LOAD_32[<BV64 rsi + 0x4>]_26[31:28]) << 0x3))>...
[MAIN]  Dumped annotated ASM to out/asm
[MAIN]  Dumped properties to out/gadgets.csv
[MAIN]  --------------- ANALYZING TFPs ------------------

real    0m3.311s
user    0m3.549s
sys     0m1.601s
➜ time ../../inspectre reason out/gadgets.csv out/gadgets-reasoned.csv
[-] Imported 4 gadgets
[-] Performing exploitability analysis...
Found 0 exploitable gadgets!
[-] Performing exploitability analysis including branch constraints...
Found 0 exploitable gadgets!
[-] Performing exploitability analysis assuming the SLAM covert channel...
Found 0 exploitable gadgets!
[-] Saving to out/gadgets-reasoned.csv
[-] Done!

real    0m0.720s
user    0m1.009s
sys     0m1.528s