diff --git a/compiler/test_else_return/example.hard.s b/compiler/test_else_return/example.hard.s new file mode 100644 index 0000000..a5dfdc5 --- /dev/null +++ b/compiler/test_else_return/example.hard.s @@ -0,0 +1,95 @@ +.syntax unified +.thumb + +.section .text +.global _start +.type _start, %function + +_start: + mov r9, #0 + mov r10, #1 + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #1 + bne countermeasure + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_0 + add r9, r9, #1 + cmp r9, #2 + bne countermeasure + mov r0, #44 + str r0, [sp] + add r9, r9, #1 + cmp r9, #3 + bne countermeasure + b endif_0 +else_0: + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #0 + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_1 + add r9, r9, #1 + cmp r9, #2 + bne countermeasure + mov r0, #33 + str r0, [sp] + add r9, r9, #1 + cmp r9, #3 + bne countermeasure + b endif_1 +else_1: +endif_1: + mov r9, #3 +endif_0: + ldr r0, [sp, #0] + mov r7, #1 + svc #0 +countermeasure: + mov r0, #1 + ldr r1, =.Lstr0 + mov r2, #14 + mov r7, #4 + svc #0 + mov r0, #77 + mov r7, #1 + svc #0 + +.size _start, .-_start + +.section .data +.Lstr0: + .ascii "COUNTERMEASURE" +step_counter: + .word 0 +fault_msg: + .ascii "Control flow violation detected\n" +_metadata: + .word 0x10000000 @ 0 + .word 0xa+3 + .word 0xb+8 + .word 0x0 @ [r0] + .word 0x00000001 @ value + .word 0x10000000 @ 1 + .word 0xa+21 + .word 0xb+25 + .word 0x0 @ [r0] + .word 0x00000001 @ value + .word 0x10000000 @ 2 + .word 0xa+40 + .word 0xb+44 + .word 0x0 @ [r0] + .word 0x00000001 @ value diff --git a/compiler/test_else_return/example.hard.wh b/compiler/test_else_return/example.hard.wh new file mode 100644 index 0000000..d02911a --- /dev/null +++ b/compiler/test_else_return/example.hard.wh @@ -0,0 +1,60 @@ +ui32 res; +ui32 stmt; +ui32 bit_shift; +ui32 flip_mask; + +fn main(ui32 stmt, ui32 flip_mask) -> ui32 { + ui32 value; + ui32 step_counter; + step_counter = (0 as ui32); + value = (0 as ui32); + if (stmt == (0 as ui32)) { + value = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (1 as ui32)) { + return (77 as ui32); + } + if ( value == (1 as ui32)) { + step_counter++; + if (step_counter != (2 as ui32)) { + return (77 as ui32); + } + value = (44 as ui32); + if (stmt == (1 as ui32)) { + value = (44 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (3 as ui32)) { + return (77 as ui32); + } + } + else { + if ( value == (0 as ui32)) { + step_counter++; + if (step_counter != (2 as ui32)) { + return (77 as ui32); + } + value = (33 as ui32); + if (stmt == (2 as ui32)) { + value = (33 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (3 as ui32)) { + return (77 as ui32); + } + } + step_counter = (3 as ui32); + } + return (value as ui32); +} +stmt = (? as ui32); +bit_shift = (? as ui32); +assume (bit_shift <= (31 as ui32)); +assume (bit_shift >= (0 as ui32)); +assume (stmt >= (0 as ui32)); +assume (stmt <= (3 as ui32)); +flip_mask = ((1 as ui32) << bit_shift); + +res = main(stmt, flip_mask); +assert(res == (0 as ui32)); diff --git a/compiler/test_else_return/test.trv b/compiler/test_else_return/example.trv similarity index 100% rename from compiler/test_else_return/test.trv rename to compiler/test_else_return/example.trv diff --git a/example_code_for_report/out.s b/example_code_for_report/out.s index fce185f..0d79364 100644 --- a/example_code_for_report/out.s +++ b/example_code_for_report/out.s @@ -36,11 +36,10 @@ else_0: b endif_1 else_1: endif_1: +endif_0: ldr r0, [sp, #0] mov r7, #1 svc #0 -endif_0: - add sp, sp, #4 .size _start, .-_start _metadata: diff --git a/example_code_for_report/out.wh b/example_code_for_report/out.wh index 692f0b2..4530c1a 100644 --- a/example_code_for_report/out.wh +++ b/example_code_for_report/out.wh @@ -22,8 +22,8 @@ fn main(ui32 stmt, ui32 flip_mask) -> ui32 { value = (33 as ui32) ^ flip_mask; } } - return (value as ui32); } + return (value as ui32); } stmt = (? as ui32); bit_shift = (? as ui32); @@ -34,4 +34,4 @@ assume (stmt <= (3 as ui32)); flip_mask = ((1 as ui32) << bit_shift); res = main(stmt, flip_mask); -assert(res == (0 as ui32)); +assert(res == (33 as ui32)); diff --git a/interpreter/src/interpreter.rs b/interpreter/src/interpreter.rs index 9909385..a2d968c 100644 --- a/interpreter/src/interpreter.rs +++ b/interpreter/src/interpreter.rs @@ -962,19 +962,23 @@ impl Interpreter { } } + let mut is_sp = false; if base_reg_name == "sp" { + is_sp = true; base_addr = self.memory.get_sp(); } else if let Some(reg_num) = base_reg_name.strip_prefix('r') { let reg_idx: usize = reg_num.parse().expect("Failed to parse register index"); base_addr = self.get_reg(reg_idx) as usize; } - let effective_addr = ((base_addr as i32) + offset) as usize; + let effective_addr = (base_addr as i32 + offset) as usize; - if effective_addr < self.memory.heap.len() { - self.memory.heap[effective_addr] = value; - } else if effective_addr < self.memory.stack.len() { + if !is_sp{ + self.memory.write_heap(effective_addr, value); + self.set_reg(base_addr, value as i32); + } else { self.memory.stack[effective_addr] = value; + self.memory.write_stack32(effective_addr, value as u32); } } diff --git a/testing/config.toml b/testing/config.toml index 6b9f905..9d7d199 100644 --- a/testing/config.toml +++ b/testing/config.toml @@ -1,5 +1,5 @@ test_folder = "pinny" -plotmode = "save" # show, save or both +plotmode = "both" # show, save or both injection_points = [ "r0", "r1", "r2", "r3", "r4", "r5", "r6", "r7", diff --git a/testing/src/plotenator.py b/testing/src/plotenator.py index d293dd5..f2348c3 100644 --- a/testing/src/plotenator.py +++ b/testing/src/plotenator.py @@ -16,8 +16,22 @@ def create_plots(self): def plot_exhaustive(self): df = self.db.query_df("SELECT * FROM exhaustive_interpreter_results") + # Group by variant and passed grouped = df.groupby(["variant", "passed"]).size().unstack(fill_value=0) + # Map the numeric passed values to descriptive labels + passed_labels = { + 0: "Faulty", + 1: "Normal Execution", + 2: "Panicked!", + 77: "Countermeasure Activated", + 78: "Faulty Jump to Countermeasure" + } + + # Rename the columns + grouped = grouped.rename(columns=passed_labels) + + # Plot fig, ax = plt.subplots() grouped.plot(kind="bar", stacked=False, ax=ax) @@ -25,7 +39,7 @@ def plot_exhaustive(self): ax.set_ylabel("Count (log scale)") ax.set_xlabel("Variant") ax.set_yscale("log") - ax.legend(title="Passed value") + ax.legend(title="Outcome") self._style_axes(ax) @@ -36,7 +50,19 @@ def plot_guided(self): grouped = df.groupby(["variant", "passed"]).size().unstack(fill_value=0) + # Map the numeric passed values to descriptive labels + passed_labels = { + 0: "Faulty", + 1: "Normal Execution", + 2: "Panicked!", + 77: "Countermeasure Activated", + 78: "Faulty Jump to Countermeasure" + } + + grouped = grouped.rename(columns=passed_labels) + fig, ax = plt.subplots() + grouped.plot(kind="bar", stacked=False, ax=ax) ax.set_title("Guided Interpreter - Outcome Distribution") @@ -68,4 +94,4 @@ def _style_axes(self, ax): # text.set_fontweight('bold') def export_symex_csv(self, output_path): df = self.db.query_df("SELECT * FROM symex_results") - df.to_csv(output_path, index=False) \ No newline at end of file + df.to_csv(output_path, index=False) diff --git a/testing/src/testrunner.py b/testing/src/testrunner.py index 6d3c3c1..965206f 100644 --- a/testing/src/testrunner.py +++ b/testing/src/testrunner.py @@ -370,17 +370,17 @@ def _generate_injection_points(self, asm_path): if len(pc_points) > 0: if pc_points[0] == "ALL": for pc in range(1, max_pc): - for bit in range(0, 31): + for bit in range(0, 32): injection_points.append(f"pc:{pc}:{bit}") else: for pc in pc_points: - for bit in range(0, 31): + for bit in range(0, 32): injection_points.append(f"pc:{pc}:{bit}") if len(registers) > 0: for pc in range(1, max_pc): for reg in registers: - for bit in range(0, 31): + for bit in range(0, 32): injection_points.append(f"reg:{pc}:{reg}:{bit}") if len(cpsr_registers) > 0: @@ -423,7 +423,7 @@ def _symex_to_injection_points(self, variant, asm_path, minimc_res): ip = f"reg:{pc}:{reg}:{bit}" injection_points.append(ip) for pc in range(start_pc, end_pc+1): - for bit in range(0, 31): + for bit in range(0, 32): ip = f"pc:{pc}:{bit}" injection_points.append(ip) for cpsr in ["n","v","z","c"]: diff --git a/testing/test b/testing/test index b87ff37..2bd702d 100755 --- a/testing/test +++ b/testing/test @@ -91,7 +91,6 @@ class Experiment: plotter = Plotter(self.db) plots = plotter.create_plots() - print("Running plots...") plots_dir = os.path.join(self.run_folder, "plots") os.makedirs(plots_dir, exist_ok=True) @@ -102,25 +101,17 @@ class Experiment: path = os.path.join(plots_dir, f"{name}.svg") fig.savefig(path, format="svg", bbox_inches="tight") - def show_plot(fig): - """Handles the rendering and cleanup of the figure.""" - plt.figure(fig.number) - plt.show() - plt.close(fig) - - - # only these remain as plots if self.plot_mode == "save" or self.plot_mode == "both": save_plot("exhaustive", plots["exhaustive"]) save_plot("guided", plots["guided"]) if self.plot_mode == "show" or self.plot_mode == "both": - show_plot(plots["exhaustive"]) - show_plot(plots["guided"]) - + plt.show() + for fig in plots.values(): + plt.close(fig) - # NEW: symex exported as CSV instead of plot + # symex exported as CSV instead of plot symex_csv_path = os.path.join(plots_dir, "symex_results.csv") plotter.export_symex_csv(symex_csv_path) diff --git a/testing/test_results/compiled_test_files/pinny.hard.s b/testing/test_results/compiled_test_files/pinny.hard.s new file mode 100644 index 0000000..c81165a --- /dev/null +++ b/testing/test_results/compiled_test_files/pinny.hard.s @@ -0,0 +1,280 @@ +.syntax unified +.thumb + +.section .text +.global _start +.type _start, %function + +_start: + mov r9, #0 + mov r10, #1 + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #1 + bne countermeasure + sub sp, sp, #4 + mov r0, #1 + str r0, [sp] + add r9, r9, #1 + cmp r9, #2 + bne countermeasure + sub sp, sp, #4 + mov r0, #2 + str r0, [sp] + add r9, r9, #1 + cmp r9, #3 + bne countermeasure + sub sp, sp, #4 + mov r0, #3 + str r0, [sp] + add r9, r9, #1 + cmp r9, #4 + bne countermeasure + sub sp, sp, #4 + mov r0, #4 + str r0, [sp] + add r9, r9, #1 + cmp r9, #5 + bne countermeasure + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #6 + bne countermeasure + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #7 + bne countermeasure + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #8 + bne countermeasure + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #9 + bne countermeasure + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #10 + bne countermeasure + ldr r0, [sp, #16] + mov r1, r0 + ldr r0, [sp, #32] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_0 + add r9, r9, #1 + cmp r9, #11 + bne countermeasure + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #12 + bne countermeasure + b endif_0 +else_0: +endif_0: + ldr r0, [sp, #12] + mov r1, r0 + ldr r0, [sp, #28] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_1 + add r9, r9, #1 + cmp r9, #13 + bne countermeasure + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #14 + bne countermeasure + b endif_1 +else_1: +endif_1: + ldr r0, [sp, #8] + mov r1, r0 + ldr r0, [sp, #24] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_2 + add r9, r9, #1 + cmp r9, #15 + bne countermeasure + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #16 + bne countermeasure + b endif_2 +else_2: +endif_2: + ldr r0, [sp, #4] + mov r1, r0 + ldr r0, [sp, #20] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_3 + add r9, r9, #1 + cmp r9, #17 + bne countermeasure + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + add r9, r9, #1 + cmp r9, #18 + bne countermeasure + b endif_3 +else_3: +endif_3: + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #4 + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_4 + add r9, r9, #1 + cmp r9, #19 + bne countermeasure + mov r0, #1 + str r0, [sp, #36] + add r9, r9, #1 + cmp r9, #20 + bne countermeasure + b endif_4 +else_4: +endif_4: + ldr r0, [sp, #36] + mov r7, #1 + svc #0 +countermeasure: + mov r0, #1 + ldr r1, =.Lstr0 + mov r2, #14 + mov r7, #4 + svc #0 + mov r0, #77 + mov r7, #1 + svc #0 + +.size _start, .-_start + +.section .data +.Lstr0: + .ascii "COUNTERMEASURE" +step_counter: + .word 0 +fault_msg: + .ascii "Control flow violation detected\n" +_metadata: + .word 0x10000000 @ 0 + .word 0xa+3 + .word 0xb+8 + .word 0x0 @ [r0] + .word 0x00000001 @ authenticated + .word 0x10000000 @ 1 + .word 0xa+9 + .word 0xb+14 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin1 + .word 0x10000000 @ 2 + .word 0xa+15 + .word 0xb+20 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin2 + .word 0x10000000 @ 3 + .word 0xa+21 + .word 0xb+26 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin3 + .word 0x10000000 @ 4 + .word 0xa+27 + .word 0xb+32 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin4 + .word 0x10000000 @ 5 + .word 0xa+33 + .word 0xb+38 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin1 + .word 0x10000000 @ 6 + .word 0xa+39 + .word 0xb+44 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin2 + .word 0x10000000 @ 7 + .word 0xa+45 + .word 0xb+50 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin3 + .word 0x10000000 @ 8 + .word 0xa+51 + .word 0xb+56 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin4 + .word 0x10000000 @ 9 + .word 0xa+57 + .word 0xb+62 + .word 0x0 @ [r0] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 10 + .word 0xa+75 + .word 0xb+82 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 11 + .word 0xa+98 + .word 0xb+105 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 12 + .word 0xa+121 + .word 0xb+128 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 13 + .word 0xa+144 + .word 0xb+151 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 14 + .word 0xa+167 + .word 0xb+171 + .word 0x0 @ [r0] + .word 0x00000001 @ authenticated diff --git a/testing/test_results/compiled_test_files/pinny.hard.wh b/testing/test_results/compiled_test_files/pinny.hard.wh new file mode 100644 index 0000000..f45bbec --- /dev/null +++ b/testing/test_results/compiled_test_files/pinny.hard.wh @@ -0,0 +1,180 @@ +ui32 res; +ui32 stmt; +ui32 bit_shift; +ui32 flip_mask; + +fn main(ui32 stmt, ui32 flip_mask) -> ui32 { + ui32 authenticated; + ui32 cardPin1; + ui32 cardPin2; + ui32 cardPin3; + ui32 cardPin4; + ui32 userPin1; + ui32 userPin2; + ui32 userPin3; + ui32 userPin4; + ui32 pinsEqual; + ui32 step_counter; + step_counter = (0 as ui32); + authenticated = (0 as ui32); + if (stmt == (0 as ui32)) { + authenticated = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (1 as ui32)) { + return (77 as ui32); + } + cardPin1 = (1 as ui32); + if (stmt == (1 as ui32)) { + cardPin1 = (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (2 as ui32)) { + return (77 as ui32); + } + cardPin2 = (2 as ui32); + if (stmt == (2 as ui32)) { + cardPin2 = (2 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (3 as ui32)) { + return (77 as ui32); + } + cardPin3 = (3 as ui32); + if (stmt == (3 as ui32)) { + cardPin3 = (3 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (4 as ui32)) { + return (77 as ui32); + } + cardPin4 = (4 as ui32); + if (stmt == (4 as ui32)) { + cardPin4 = (4 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (5 as ui32)) { + return (77 as ui32); + } + userPin1 = (0 as ui32); + if (stmt == (5 as ui32)) { + userPin1 = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (6 as ui32)) { + return (77 as ui32); + } + userPin2 = (0 as ui32); + if (stmt == (6 as ui32)) { + userPin2 = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (7 as ui32)) { + return (77 as ui32); + } + userPin3 = (0 as ui32); + if (stmt == (7 as ui32)) { + userPin3 = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (8 as ui32)) { + return (77 as ui32); + } + userPin4 = (0 as ui32); + if (stmt == (8 as ui32)) { + userPin4 = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (9 as ui32)) { + return (77 as ui32); + } + pinsEqual = (0 as ui32); + if (stmt == (9 as ui32)) { + pinsEqual = (0 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (10 as ui32)) { + return (77 as ui32); + } + if ( userPin1 == cardPin1) { + step_counter++; + if (step_counter != (11 as ui32)) { + return (77 as ui32); + } + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (10 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (12 as ui32)) { + return (77 as ui32); + } + } + if ( userPin2 == cardPin2) { + step_counter++; + if (step_counter != (13 as ui32)) { + return (77 as ui32); + } + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (11 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (14 as ui32)) { + return (77 as ui32); + } + } + if ( userPin3 == cardPin3) { + step_counter++; + if (step_counter != (15 as ui32)) { + return (77 as ui32); + } + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (12 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (16 as ui32)) { + return (77 as ui32); + } + } + if ( userPin4 == cardPin4) { + step_counter++; + if (step_counter != (17 as ui32)) { + return (77 as ui32); + } + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (13 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (18 as ui32)) { + return (77 as ui32); + } + } + if ( pinsEqual == (4 as ui32)) { + step_counter++; + if (step_counter != (19 as ui32)) { + return (77 as ui32); + } + authenticated = (1 as ui32); + if (stmt == (14 as ui32)) { + authenticated = (1 as ui32) ^ flip_mask; + } + step_counter++; + if (step_counter != (20 as ui32)) { + return (77 as ui32); + } + } + return (authenticated as ui32); +} +stmt = (? as ui32); +bit_shift = (? as ui32); +assume (bit_shift <= (31 as ui32)); +assume (bit_shift >= (0 as ui32)); +assume (stmt >= (0 as ui32)); +assume (stmt <= (15 as ui32)); +flip_mask = ((1 as ui32) << bit_shift); + +res = main(stmt, flip_mask); +assert(res == (0 as ui32)); diff --git a/testing/test_results/compiled_test_files/pinny.s b/testing/test_results/compiled_test_files/pinny.s new file mode 100644 index 0000000..c6aa62b --- /dev/null +++ b/testing/test_results/compiled_test_files/pinny.s @@ -0,0 +1,201 @@ +.syntax unified +.thumb + +.section .text +.global _start +.type _start, %function + +_start: + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + sub sp, sp, #4 + mov r0, #1 + str r0, [sp] + sub sp, sp, #4 + mov r0, #2 + str r0, [sp] + sub sp, sp, #4 + mov r0, #3 + str r0, [sp] + sub sp, sp, #4 + mov r0, #4 + str r0, [sp] + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + sub sp, sp, #4 + mov r0, #0 + str r0, [sp] + ldr r0, [sp, #16] + mov r1, r0 + ldr r0, [sp, #32] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_0 + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + b endif_0 +else_0: +endif_0: + ldr r0, [sp, #12] + mov r1, r0 + ldr r0, [sp, #28] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_1 + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + b endif_1 +else_1: +endif_1: + ldr r0, [sp, #8] + mov r1, r0 + ldr r0, [sp, #24] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_2 + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + b endif_2 +else_2: +endif_2: + ldr r0, [sp, #4] + mov r1, r0 + ldr r0, [sp, #20] + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_3 + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #1 + add r0, r1, r0 + str r0, [sp] + b endif_3 +else_3: +endif_3: + ldr r0, [sp, #0] + mov r1, r0 + mov r0, #4 + cmp r1, r0 + mov r0, #0 + it eq + moveq r0, #1 + cmp r0, #0 + beq else_4 + mov r0, #1 + str r0, [sp, #36] + b endif_4 +else_4: +endif_4: + ldr r0, [sp, #36] + mov r7, #1 + svc #0 + +.size _start, .-_start +_metadata: + .word 0x10000000 @ 0 + .word 0xa+1 + .word 0xb+3 + .word 0x0 @ [r0] + .word 0x00000001 @ authenticated + .word 0x10000000 @ 1 + .word 0xa+4 + .word 0xb+6 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin1 + .word 0x10000000 @ 2 + .word 0xa+7 + .word 0xb+9 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin2 + .word 0x10000000 @ 3 + .word 0xa+10 + .word 0xb+12 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin3 + .word 0x10000000 @ 4 + .word 0xa+13 + .word 0xb+15 + .word 0x0 @ [r0] + .word 0x00000001 @ cardPin4 + .word 0x10000000 @ 5 + .word 0xa+16 + .word 0xb+18 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin1 + .word 0x10000000 @ 6 + .word 0xa+19 + .word 0xb+21 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin2 + .word 0x10000000 @ 7 + .word 0xa+22 + .word 0xb+24 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin3 + .word 0x10000000 @ 8 + .word 0xa+25 + .word 0xb+27 + .word 0x0 @ [r0] + .word 0x00000001 @ userPin4 + .word 0x10000000 @ 9 + .word 0xa+28 + .word 0xb+30 + .word 0x0 @ [r0] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 10 + .word 0xa+40 + .word 0xb+44 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 11 + .word 0xa+57 + .word 0xb+61 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 12 + .word 0xa+74 + .word 0xb+78 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 13 + .word 0xa+91 + .word 0xb+95 + .word 0x0 @ [r0,r1] + .word 0x00000001 @ pinsEqual + .word 0x10000000 @ 14 + .word 0xa+108 + .word 0xb+109 + .word 0x0 @ [r0] + .word 0x00000001 @ authenticated diff --git a/testing/test_results/compiled_test_files/pinny.wh b/testing/test_results/compiled_test_files/pinny.wh new file mode 100644 index 0000000..55fd9c0 --- /dev/null +++ b/testing/test_results/compiled_test_files/pinny.wh @@ -0,0 +1,98 @@ +ui32 res; +ui32 stmt; +ui32 bit_shift; +ui32 flip_mask; + +fn main(ui32 stmt, ui32 flip_mask) -> ui32 { + ui32 authenticated; + ui32 cardPin1; + ui32 cardPin2; + ui32 cardPin3; + ui32 cardPin4; + ui32 userPin1; + ui32 userPin2; + ui32 userPin3; + ui32 userPin4; + ui32 pinsEqual; + authenticated = (0 as ui32); + if (stmt == (0 as ui32)) { + authenticated = (0 as ui32) ^ flip_mask; + } + cardPin1 = (1 as ui32); + if (stmt == (1 as ui32)) { + cardPin1 = (1 as ui32) ^ flip_mask; + } + cardPin2 = (2 as ui32); + if (stmt == (2 as ui32)) { + cardPin2 = (2 as ui32) ^ flip_mask; + } + cardPin3 = (3 as ui32); + if (stmt == (3 as ui32)) { + cardPin3 = (3 as ui32) ^ flip_mask; + } + cardPin4 = (4 as ui32); + if (stmt == (4 as ui32)) { + cardPin4 = (4 as ui32) ^ flip_mask; + } + userPin1 = (0 as ui32); + if (stmt == (5 as ui32)) { + userPin1 = (0 as ui32) ^ flip_mask; + } + userPin2 = (0 as ui32); + if (stmt == (6 as ui32)) { + userPin2 = (0 as ui32) ^ flip_mask; + } + userPin3 = (0 as ui32); + if (stmt == (7 as ui32)) { + userPin3 = (0 as ui32) ^ flip_mask; + } + userPin4 = (0 as ui32); + if (stmt == (8 as ui32)) { + userPin4 = (0 as ui32) ^ flip_mask; + } + pinsEqual = (0 as ui32); + if (stmt == (9 as ui32)) { + pinsEqual = (0 as ui32) ^ flip_mask; + } + if ( userPin1 == cardPin1) { + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (10 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + } + if ( userPin2 == cardPin2) { + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (11 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + } + if ( userPin3 == cardPin3) { + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (12 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + } + if ( userPin4 == cardPin4) { + pinsEqual = pinsEqual + (1 as ui32); + if (stmt == (13 as ui32)) { + pinsEqual = pinsEqual + (1 as ui32) ^ flip_mask; + } + } + if ( pinsEqual == (4 as ui32)) { + authenticated = (1 as ui32); + if (stmt == (14 as ui32)) { + authenticated = (1 as ui32) ^ flip_mask; + } + } + return (authenticated as ui32); +} +stmt = (? as ui32); +bit_shift = (? as ui32); +assume (bit_shift <= (31 as ui32)); +assume (bit_shift >= (0 as ui32)); +assume (stmt >= (0 as ui32)); +assume (stmt <= (15 as ui32)); +flip_mask = ((1 as ui32) << bit_shift); + +res = main(stmt, flip_mask); +assert(res == (0 as ui32)); diff --git a/testing/test_results/plots/exhaustive.svg b/testing/test_results/plots/exhaustive.svg new file mode 100644 index 0000000..7e8fd99 --- /dev/null +++ b/testing/test_results/plots/exhaustive.svg @@ -0,0 +1,1786 @@ + + + + + + + + 2026-05-13T13:21:49.151067 + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/testing/test_results/plots/guided.svg b/testing/test_results/plots/guided.svg new file mode 100644 index 0000000..e55561a --- /dev/null +++ b/testing/test_results/plots/guided.svg @@ -0,0 +1,1553 @@ + + + + + + + + 2026-05-13T13:21:49.294873 + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/testing/test_results/plots/symex_results.csv b/testing/test_results/plots/symex_results.csv new file mode 100644 index 0000000..370411f --- /dev/null +++ b/testing/test_results/plots/symex_results.csv @@ -0,0 +1,17 @@ +id,run_id,test,variant,stmt,faulty_bit,result +1,2,pinny,Hard,9,2,77 +2,2,pinny,Hard,8,2,77 +3,2,pinny,Hard,6,1,77 +4,2,pinny,Hard,4,2,77 +5,2,pinny,Hard,2,1,77 +6,2,pinny,Hard,0,0,1 +7,2,pinny,Normal,9,2,1 +8,2,pinny,Normal,0,0,1 +9,3,pinny,Hard,9,2,77 +10,3,pinny,Hard,8,2,77 +11,3,pinny,Hard,6,1,77 +12,3,pinny,Hard,4,2,77 +13,3,pinny,Hard,2,1,77 +14,3,pinny,Hard,0,0,1 +15,3,pinny,Normal,9,2,1 +16,3,pinny,Normal,0,0,1 diff --git a/testing/test_results/results.db b/testing/test_results/results.db new file mode 100644 index 0000000..2cae9e2 Binary files /dev/null and b/testing/test_results/results.db differ diff --git a/testing/test_results/tests/pinny.trv b/testing/test_results/tests/pinny.trv new file mode 100644 index 0000000..f14b225 --- /dev/null +++ b/testing/test_results/tests/pinny.trv @@ -0,0 +1,34 @@ +func main() -> Integer { + let authenticated : Integer = 0; + let cardPin1 : Integer = 1; + let cardPin2 : Integer = 2; + let cardPin3 : Integer = 3; + let cardPin4 : Integer = 4; + let userPin1 : Integer = 0; + let userPin2 : Integer = 0; + let userPin3 : Integer = 0; + let userPin4 : Integer = 0; + let pinsEqual : Integer = 0; + + if userPin1 == cardPin1 then { + pinsEqual = pinsEqual + 1; + } + + if userPin2 == cardPin2 then { + pinsEqual = pinsEqual + 1; + } + + if userPin3 == cardPin3 then { + pinsEqual = pinsEqual + 1; + } + + if userPin4 == cardPin4 then { + pinsEqual = pinsEqual + 1; + } + + if pinsEqual == 4 then { + authenticated = 1; + } + + return authenticated; +} diff --git a/testing/test_results/tests/pinny.trv.output b/testing/test_results/tests/pinny.trv.output new file mode 100644 index 0000000..e69de29 diff --git a/testing/test_results/tests/pinny.wh b/testing/test_results/tests/pinny.wh new file mode 100644 index 0000000..4abe1e9 --- /dev/null +++ b/testing/test_results/tests/pinny.wh @@ -0,0 +1,103 @@ +ui32 res; +ui32 stmt; +ui32 bit_shift; +ui32 flip_mask; + +fn main(ui32 stmt, ui32 flip_mask) -> ui32 { + ui32 ptc; + ui32 authenticated; + ui32 cardPin1; + ui32 cardPin2; + ui32 cardPin3; + ui32 cardPin4; + ui32 userPin1; + ui32 userPin2; + ui32 userPin3; + ui32 userPin4; + ui32 pinsEqual; + authenticated = (0 as ui32); + if(stmt == (1 as ui32)) { + authenticated = (0 as ui32) ^ flip_mask; + } + cardPin1 = (1 as ui32); + if(stmt == (2 as ui32)) { + cardPin1 = (1 as ui32) ^ flip_mask; + } + cardPin2 = (2 as ui32); + if(stmt == (3 as ui32)) { + cardPin2 = (2 as ui32) ^ flip_mask; + } + cardPin3 = (3 as ui32); + if(stmt == (4 as ui32)) { + cardPin3 = (3 as ui32) ^ flip_mask; + } + cardPin4 = (4 as ui32); + if(stmt == (5 as ui32)) { + cardPin4 = (4 as ui32) ^ flip_mask; + } + userPin1 = (0 as ui32); + if(stmt == (6 as ui32)) { + userPin1 = (0 as ui32) ^ flip_mask; + } + userPin2 = (0 as ui32); + if(stmt == (7 as ui32)) { + userPin2 = (0 as ui32) ^ flip_mask; + } + userPin3 = (0 as ui32); + if(stmt == (8 as ui32)) { + userPin3 = (0 as ui32) ^ flip_mask; + } + userPin4 = (0 as ui32); + if(stmt == (9 as ui32)) { + userPin4 = (0 as ui32) ^ flip_mask; + } + pinsEqual = (0 as ui32); + if(stmt == (10 as ui32)) { + pinsEqual = (0 as ui32) ^ flip_mask; + } + + if ( userPin1 == cardPin1) { + pinsEqual++; + if(stmt == (11 as ui32)) { + pinsEqual = pinsEqual ^ flip_mask; + } + } + + if ( userPin2 == cardPin2) { + pinsEqual++; + if(stmt == (12 as ui32)) { + pinsEqual = pinsEqual ^ flip_mask; + } + } + if ( userPin3 == cardPin3) { + pinsEqual++; + if(stmt == (13 as ui32)) { + pinsEqual = pinsEqual ^ flip_mask; + } + } + + if ( userPin4 == cardPin4) { + pinsEqual++; + if(stmt == (14 as ui32)) { + pinsEqual = pinsEqual ^ flip_mask; + } + } + + if ( pinsEqual == (4 as ui32)) { + authenticated = (1 as ui32); + if(stmt == (14 as ui32)) { + authenticated = (1 as ui32) ^ flip_mask; + } + } + return (authenticated as ui32); +} + +stmt = (? as ui32); +bit_shift = (? as ui32); +assume (bit_shift <= (31 as ui32)); +assume (bit_shift >= (0 as ui32)); +assume (stmt >= (1 as ui32)); +assume (stmt <= (14 as ui32)); +flip_mask = ((1 as ui32) << bit_shift); +res = main(stmt, flip_mask); +assert(res == (0 as ui32));