Tests for the journal version

README.md

@@ -2,12 +2,16 @@
 
 This repository contains the benchmarks from the papers "Spectector:
 Principled Detection of Speculative Information Flows" (available
-[here](https://spectector.github.io/papers/spectector.pdf)) and 
+[here](https://spectector.github.io/papers/spectector.pdf)), 
 "Hardware/software contracts for secure speculation" (available
-[here](https://spectector.github.io/papers/hwsw-contracts.pdf)). 
+[here](https://spectector.github.io/papers/hwsw-contracts.pdf))
+and the journal version 
+"Detecting speculative leaks with compositional semantics" (available
+[here](https://spectector.github.io/papers/journal.pdf))
 
 Here we describe how to reproduce the experimental results from the
 Spectector's paper. For the hardware/software contracts paper, see the `hwsw-contracts` folder.
+For the journal paper see the `journal` folder as well.
 
 ## Case Study: Compiler countermeasures (Section VIII)
 

journal/README.md

@@ -0,0 +1,25 @@
+# Tests
+
+These are the additonal tests for Spectre versions different from V1.
+The V1 test cases can be found the sources folder.
+
+There are sub-folders v4_tests, v5_tests, v2_tests, sls_tests and combinations_tests containing examples. Each sub-folder provides its own script to execute all the tests inside it. They are also a pointer on how to use the tool. Some sub-folders have additional README files with more information.
+
+
+The different versions can be selected using the --version flag. The different versions are:
+
+- 1 : V1 (original implementation of Spectector)
+- 2 : Spectre V2
+- 4 : Spectre V4
+- 5 : Spectre V5
+- 6 : Spectre SLS
+
+and any combination of those versions that are allowed. Versions that are not allowed are combinations of 5 and 6, because they speculate on the same instructions. More details in the paper. For example:
+
+- 14 : Spectre V1 + Spectre V4
+- 45 : V4 + V5
+- 15 : V1 + V5
+- 145: V1 + V4 + V5
+- 1245 : V1 + V2 + V4 + V5
+
+See the provided scripts to see examples for the usage.

journal/combinations_tests/README.md

@@ -0,0 +1,11 @@
+We sometimes added the construct
+load f, secret % set up a secret
+store f, 1
+spbarr
+
+to some test cases. This is done to set up a secret for Spectector and does not influence the vulnerability. For Spectector all memory regions are high values and all registers are low.
+The problem is that we cannot specify the value secret to be high. There is no option for that. So we add this snippet which means that we have a high symbolic value stored at location 1.
+
+Use the script exec_all_combs.sh to see all the combinations in action. For each of the combinations, we created an 
+example showing the additional strength.
+There is a version with a barrier inserted as well.

journal/combinations_tests/combined12.muasm

@@ -0,0 +1,12 @@
+main:
+    rax <- L2 
+    indirect_jump rax
+spec:
+    endbr
+    x <-  0
+    beqz x , L2 
+L100:
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+L2:
+    skip

journal/combinations_tests/combined124.muasm

@@ -0,0 +1,16 @@
+main:
+    load f, secret % prepare a secret 
+    store f, 0
+    spbarr
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    x <- 0
+    beqz x, L2
+    store 1, 0 % overwrite but V4
+    load eax, 0 % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined1245.muasm

@@ -0,0 +1,31 @@
+manipStack:
+    sp <- sp + 8 % pop return address so we jumo back to main
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+speculate:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp manipStack
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    x <- 0
+    beqz x, L2
+    store 1, 0 % Overwrite secret, will be skipped
+    load eax, 0 % Should never be executed
+    load edi, eax
+    spbarr
+main:
+    load f, secret % prepare a secret 
+    store f, 0
+    spbarr
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp speculate
+L2:
+    skip

journal/combinations_tests/combined1245_barrier.muasm

@@ -0,0 +1,32 @@
+manipStack:
+    sp <- sp + 8 % pop return address so we jumo back to main
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+speculate:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp manipStack
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    spbarr
+    x <- 0
+    beqz x, L2
+    store 1, 0 % Overwrite secret, will be skipped
+    load eax, 0 % Should never be executed
+    load edi, eax
+    spbarr
+main:
+    load f, secret % prepare a secret 
+    store f, 0
+    spbarr
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp speculate
+L2:
+    skip

journal/combinations_tests/combined1246.muasm

@@ -0,0 +1,23 @@
+main:
+    load f, secret
+    store f, 0
+    spbarr
+    store 1, 0 
+    eax <- 5
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+L1:
+    rax <- L2
+    indirect_jump rax
+spec:
+    endbr
+    x <-  0
+    beqz x , L2 
+L100:
+    load eax, 1 % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined1246_barrier.muasm

@@ -0,0 +1,24 @@
+main:
+    load f, secret
+    store f, 0
+    spbarr
+    store 1, 0 
+    eax <- 5
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+L1:
+    rax <- L2
+    indirect_jump rax
+spec:
+    endbr
+    spbarr
+    x <-  0
+    beqz x , L2 
+L100:
+    load eax, 1 % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined124_barrier.muasm

@@ -0,0 +1,17 @@
+main:
+    load f, secret % prepare a secret 
+    store f, 0
+    spbarr
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    spbarr
+    x <- 0
+    beqz x, L2
+    store 1, 0 % overwrite but V4
+    load eax, 0 % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined125.muasm

@@ -0,0 +1,27 @@
+manipStack:
+    sp <- sp + 8 % pop return address so we jumo back to main
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+speculate:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp manipStack
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    x <- 0
+    beqz x, L2
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+    spbarr
+main:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp speculate
+L2:
+    skip

journal/combinations_tests/combined125_barrier.muasm

@@ -0,0 +1,28 @@
+manipStack:
+    sp <- sp + 8 % pop return address so we jumo back to main
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+speculate:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp manipStack
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    spbarr
+    x <- 0
+    beqz x, L2
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+    spbarr
+main:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp speculate
+L2:
+    skip

journal/combinations_tests/combined126.muasm

@@ -0,0 +1,17 @@
+main:
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+spec:
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    x <- 0
+    beqz x, L2
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined126_barrier.muasm

@@ -0,0 +1,18 @@
+main:
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+spec:
+    rax <- L2 % Spec v5 reaches here
+    indirect_jump rax
+L100:
+    endbr
+    spbarr
+    x <- 0
+    beqz x, L2
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+    spbarr
+L2:
+    skip

journal/combinations_tests/combined12_barrier.muasm

@@ -0,0 +1,13 @@
+main:
+    rax <- L2 
+    indirect_jump rax
+spec:
+    endbr
+    x <-  0
+    beqz x , L2 
+    spbarr
+L100:
+    load eax, secret_addr % Should never be executed
+    load edi, eax
+L2:
+    skip

journal/combinations_tests/combined14.muasm

@@ -0,0 +1,16 @@
+
+
+
+main:
+    load f, secret % set up a secret for spectector
+	store f, 1
+    spbarr
+    store 0, 1 % overwrite the secret in memory
+	x <- 0
+	beqz x, L1
+L2:
+	load x, 1
+	load eax, x % This should show us the secret value
+	spbarr
+L1:
+	skip

journal/combinations_tests/combined145.muasm

@@ -0,0 +1,31 @@
+manipStack:
+    sp <- sp + 8 % pop return address so we jumo back to main
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+speculate:
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp manipStack
+    x <-  0
+    beqz x , L2
+L100:
+    load eax, 0 % leak secret
+    load edi, eax
+L2:
+    spbarr
+    retstart
+    load tmp,sp/\140737488355327
+    sp<-sp+8
+    jmp tmp
+main:
+    load f, secret % prepare a secret 
+    store f, 0
+    spbarr
+    store 1, 0 % overwrites the secret but will be skipped speculatively
+    callstart
+    sp<-sp-8
+    store pc+2, sp/\140737488355327
+    jmp speculate