InstrSem/basic_demonstration.py at main · cispa/InstrSem · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
import sys
import subprocess

def try_reverse(instruction, architecture, bytelen, depth=2, samples=500):
    try:
        cmd = ["docker", "run", "--rm", "-i", "-v", "./instr_reverser:/instr_reverser", "artifact_instrsem", "python3", "main.py", architecture, hex(instruction), "0", str(bytelen*8), str(depth), str(samples)]
        print(" ".join(cmd))
        x = subprocess.run(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.PIPE).stderr.decode()
        variable_bits = x.split("variable bits: ")[1].split("\n")[0]
        return eval(variable_bits), x
    except:
        return None, None

# --- aarch64 ---
# In the outputs you can ignore pstate=0.
# This is just an artifact of our runner implementation.

# add x1, x2, x3
print(" === add x1, x2, x3 === ")
print(try_reverse(0x8b030041, "aarch64-socket", 4)[1])

# mul x1, x2, x3
print(" === mul x1, x2, x3 === ")
print(try_reverse(0x9b037c41, "aarch64-socket", 4)[1])

# cbz x1, 0x120
# mem_value_out = 0 is an artifact of the reverser implementation.
# In the full output (which is piped to /dev/null), it is identified that the mapping requires execute protection.
# To ensure crashing after the jump, the value of the mapping is fixed to 0 (an illegal instruction on aarch64 - at least all devices we tried).
# Thus, the reverser recovers the semantics mem_val_out = 0.
print(" === cbz x1, 0x120 === ")
print(try_reverse(0xb4000901, "aarch64-socket", 4)[1])


# --- riscv-64 ---

# addi x1, x0, 1000
print(" === addi x1, x0, 1000 === " )
print(try_reverse(0x3e800093, "riscv64-socket", 4)[1])

# nop
print(" === nop === " )
print(try_reverse(0x00000013, "riscv64-socket", 4)[1])

# jal 0x134
# same mem_val_out = 0 as cbz above
print(" === jal 0x134 === ")
print(try_reverse(0x134000ef, "riscv64-socket", 4)[1])


# --- loongarch64 ---

# sltu $t0, $t1, $t2
print(" === sltu $t0, $t1, $t2 === ")
print(try_reverse(0x0012b9ac, "loongarch64-socket", 4)[1])

# bl 7992
# same mem_val_out = 0 as jal above
print(" === bl 7992 === ")
print(try_reverse(0x541f3800, "loongarch64-socket", 4)[1])

# v0 = v1 + v2 (8-bit SIMD result truncated to 128-bit)
print(" === vector simd add (8-bit) v0 = truncate to 128-bit v1 + v2 === ")
print(try_reverse(0x700a0820, "loongarch64-socket", 4)[1])


# --- x86-64 ---

# pop r8
# "gpr_new" refers to r8-r15
print(" === pop r8 === ")
print(try_reverse(0x5841, "x86_64-socket", 2)[1])

# push r9
print(" === push r9 === ")
print(try_reverse(0x5141, "x86_64-socket", 2)[1])

# mov word ptr [r9 + 0x120], 0xdeadbeef
# r9 is not clustered here because the encoding is weird
print(" === mov word ptr [r9 + 0x120], 0xdeadbeef === ")
print(try_reverse(0xbeef0000012081c74166, "x86_64-socket", 10)[1])