Unverified Commit 221b85db authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Phases (experimental)

Phases are an exciting new feature that allows Verifpal to reliably
model post-compromise security properties such as forward secrecy or
future secrecy.

When modeling with an active attacker, a new phase can be declared thus:

```
principal Alice[...]
principal Bob [...]
Bob -> Alice: b1

phase[1]

principal Alice[...]
Alice -> Bob: a2
```

In the above example, the attacker won't be able to learn a2 until the
execution of everything that occured in phase 0 (the initial phase of
any model) is concluded. Furthermore, the attacker can only manipulate
a2 within the confines of the phases in which it is communicated. That
is to say, the attacker will have knowledge of b1 when doing analysis
in phase 1, but won't be able to manipulate b1 in phase 1. The attacker
won't have knowledge of a2 during phase 0, but will be able to
manipulate b1 in phase 0.

Values are learned at the earliest phase in which they are communicated,
and can only be manipulated within phases in which they are
communicated, which can be more than one phase since Alice can for
example send a2 later to Carol, to Damian...

Importantly, values derived from mutations of b1 in phase 0 cannot be
used to construct new values in phase 1.

A pertinent example of how phases can be used has been added to the
signal.vp and signal_small.vp models, where phases are used to model
forward secrecy in the Signal Protocol for exchanges involving three
messages and one message respectively.

Phases support was already added to the Visual Studio Code and Vim
extensions in a previous commit (ad26547f) and those extensions will be
pushed onto their respective marketplaces shortly. The Verifpal User
Manual will also be updated.
parent 14e349fe
......@@ -3,7 +3,7 @@
attacker[active]
// Setup phase
// Setup
principal Alice[
knows public n
......
......@@ -88,6 +88,11 @@ principal Bob[
m3_d = AEAD_DEC(bkenc5, e3, HASH(gblongterm, galongterm, gae3))
]
phase[1]
Alice -> Bob: alongterm
Bob -> Alice: blongterm
queries[
confidentiality? m1
authentication? Alice -> Bob: e1
......
......@@ -17,7 +17,7 @@ principal Bob[
gbssig = SIGN(blongterm, gbs)
]
Bob -> Alice: gblongterm, gbssig, gbs, gbo
Bob -> Alice: [gblongterm], gbssig, gbs, gbo
principal Alice[
generates ae1
......@@ -36,7 +36,7 @@ principal Alice[
e1 = AEAD_ENC(akenc1, m1, HASH(galongterm, gblongterm, gae2))
]
Alice -> Bob: galongterm, gae1, gae2, e1
Alice -> Bob: [galongterm], gae1, gae2, e1
principal Bob[
bmaster = HASH(nil, galongterm^bs, gae1^blongterm, gae1^bs, gae1^bo)
......@@ -50,6 +50,11 @@ principal Bob[
m1_d = AEAD_DEC(bkenc1, e1, HASH(galongterm, gblongterm, gae2))
]
phase[1]
Alice ->Bob: alongterm
Bob -> Alice: blongterm
queries[
confidentiality? m1
authentication? Alice -> Bob: e1
......
......@@ -9,24 +9,35 @@ import "sync"
var attackerStateShared attackerState
var attackerStateMutex sync.Mutex
func attackerStateInit(m Model, valKnowledgeMap knowledgeMap, active bool) bool {
func attackerStateInit(active bool) {
attackerStateMutex.Lock()
attackerStateShared = attackerState{
active: active,
known: []value{},
wire: []bool{},
mutatedTo: [][]string{},
active: active,
currentPhase: 0,
known: []value{},
wire: []bool{},
mutatedTo: [][]string{},
}
for _, c := range valKnowledgeMap.constants {
if c.qualifier == "public" {
v := value{
kind: "constant",
constant: c,
}
attackerStateShared.known = append(attackerStateShared.known, v)
attackerStateShared.wire = append(attackerStateShared.wire, false)
attackerStateShared.mutatedTo = append(attackerStateShared.mutatedTo, []string{})
attackerStateMutex.Unlock()
}
func attackerStateAbsorbPhaseValues(m Model, valKnowledgeMap knowledgeMap) {
attackerStateMutex.Lock()
for i, c := range valKnowledgeMap.constants {
if c.qualifier != "public" {
continue
}
v := value{
kind: "constant",
constant: c,
}
earliestPhase, err := minIntInSlice(valKnowledgeMap.phase[i])
if err == nil && earliestPhase > attackerStateShared.currentPhase {
continue
}
attackerStateShared.known = append(attackerStateShared.known, v)
attackerStateShared.wire = append(attackerStateShared.wire, false)
attackerStateShared.mutatedTo = append(attackerStateShared.mutatedTo, []string{})
}
for _, blck := range m.blocks {
switch blck.kind {
......@@ -40,6 +51,13 @@ func attackerStateInit(m Model, valKnowledgeMap knowledgeMap, active bool) bool
if valKnowledgeMap.constants[i].qualifier != "private" {
continue
}
earliestPhase, err := minIntInSlice(valKnowledgeMap.phase[i])
if err != nil {
errorCritical(err.Error())
}
if earliestPhase > attackerStateShared.currentPhase {
continue
}
ii := sanityExactSameValueInValues(v, attackerStateShared.known)
if ii >= 0 {
attackerStateShared.wire[ii] = true
......@@ -52,7 +70,6 @@ func attackerStateInit(m Model, valKnowledgeMap knowledgeMap, active bool) bool
}
}
attackerStateMutex.Unlock()
return true
}
func attackerStateGetRead() attackerState {
......@@ -76,14 +93,20 @@ func attackerStatePutWrite(write attackerStateWrite) bool {
}
func attackerStatePutMutatedToUpdate(update attackerStateMutatedToUpdate) bool {
var err error
written := false
attackerStateMutex.Lock()
if !strInSlice(update.principal, attackerStateShared.mutatedTo[update.i]) {
written = true
attackerStateShared.mutatedTo[update.i] = append(
attackerStateShared.mutatedTo[update.i], update.principal,
)
}
attackerStateShared.mutatedTo[update.i], err = appendUniqueString(
attackerStateShared.mutatedTo[update.i], update.principal,
)
written = (err == nil)
attackerStateMutex.Unlock()
return written
}
func attackerStatePutPhaseUpdate(m Model, valKnowledgeMap knowledgeMap, phase int) {
attackerStateMutex.Lock()
attackerStateShared.currentPhase = phase
attackerStateMutex.Unlock()
attackerStateAbsorbPhaseValues(m, valKnowledgeMap)
}
......@@ -4,9 +4,7 @@
package verifpal
import (
"fmt"
)
import "fmt"
func constructKnowledgeMap(m Model, principals []string) knowledgeMap {
valKnowledgeMap := knowledgeMap{
......@@ -15,15 +13,15 @@ func constructKnowledgeMap(m Model, principals []string) knowledgeMap {
assigned: []value{},
creator: []string{},
knownBy: [][]map[string]string{},
phase: []int{},
phase: [][]int{},
unnamedCounter: 0,
}
phase := 0
currentPhase := 0
valKnowledgeMap.constants = append(valKnowledgeMap.constants, constantG.constant)
valKnowledgeMap.assigned = append(valKnowledgeMap.assigned, constantG)
valKnowledgeMap.creator = append(valKnowledgeMap.creator, principals[0])
valKnowledgeMap.knownBy = append(valKnowledgeMap.knownBy, []map[string]string{})
valKnowledgeMap.phase = append(valKnowledgeMap.phase, phase)
valKnowledgeMap.phase = append(valKnowledgeMap.phase, []int{currentPhase})
for _, principal := range principals {
valKnowledgeMap.knownBy[0] = append(
valKnowledgeMap.knownBy[0],
......@@ -34,7 +32,7 @@ func constructKnowledgeMap(m Model, principals []string) knowledgeMap {
valKnowledgeMap.assigned = append(valKnowledgeMap.assigned, constantN)
valKnowledgeMap.creator = append(valKnowledgeMap.creator, principals[0])
valKnowledgeMap.knownBy = append(valKnowledgeMap.knownBy, []map[string]string{})
valKnowledgeMap.phase = append(valKnowledgeMap.phase, phase)
valKnowledgeMap.phase = append(valKnowledgeMap.phase, []int{currentPhase})
for _, principal := range principals {
valKnowledgeMap.knownBy[1] = append(
valKnowledgeMap.knownBy[1],
......@@ -48,31 +46,32 @@ func constructKnowledgeMap(m Model, principals []string) knowledgeMap {
switch expr.kind {
case "knows":
valKnowledgeMap = constructKnowledgeMapRenderKnows(
valKnowledgeMap, blck, expr, phase,
valKnowledgeMap, blck, expr,
)
case "generates":
valKnowledgeMap = constructKnowledgeMapRenderGenerates(
valKnowledgeMap, blck, expr, phase,
valKnowledgeMap, blck, expr,
)
case "assignment":
valKnowledgeMap = constructKnowledgeMapRenderAssignment(
valKnowledgeMap, blck, expr, phase,
valKnowledgeMap, blck, expr,
)
}
}
case "message":
valKnowledgeMap = constructKnowledgeMapRenderMessage(
valKnowledgeMap, blck,
valKnowledgeMap, blck, currentPhase,
)
case "phase":
phase = blck.phase.number
currentPhase = blck.phase.number
}
}
valKnowledgeMap.maxPhase = currentPhase
return valKnowledgeMap
}
func constructKnowledgeMapRenderKnows(
valKnowledgeMap knowledgeMap, blck block, expr expression, phase int,
valKnowledgeMap knowledgeMap, blck block, expr expression,
) knowledgeMap {
for _, c := range expr.constants {
i := sanityGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
......@@ -108,7 +107,7 @@ func constructKnowledgeMapRenderKnows(
})
valKnowledgeMap.creator = append(valKnowledgeMap.creator, blck.principal.name)
valKnowledgeMap.knownBy = append(valKnowledgeMap.knownBy, []map[string]string{})
valKnowledgeMap.phase = append(valKnowledgeMap.phase, phase)
valKnowledgeMap.phase = append(valKnowledgeMap.phase, []int{})
l := len(valKnowledgeMap.constants) - 1
if expr.qualifier != "public" {
continue
......@@ -126,7 +125,7 @@ func constructKnowledgeMapRenderKnows(
}
func constructKnowledgeMapRenderGenerates(
valKnowledgeMap knowledgeMap, blck block, expr expression, phase int,
valKnowledgeMap knowledgeMap, blck block, expr expression,
) knowledgeMap {
for _, c := range expr.constants {
i := sanityGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
......@@ -151,13 +150,13 @@ func constructKnowledgeMapRenderGenerates(
})
valKnowledgeMap.creator = append(valKnowledgeMap.creator, blck.principal.name)
valKnowledgeMap.knownBy = append(valKnowledgeMap.knownBy, []map[string]string{{}})
valKnowledgeMap.phase = append(valKnowledgeMap.phase, phase)
valKnowledgeMap.phase = append(valKnowledgeMap.phase, []int{})
}
return valKnowledgeMap
}
func constructKnowledgeMapRenderAssignment(
valKnowledgeMap knowledgeMap, blck block, expr expression, phase int,
valKnowledgeMap knowledgeMap, blck block, expr expression,
) knowledgeMap {
constants := sanityAssignmentConstants(expr.right, []constant{}, valKnowledgeMap)
switch expr.right.kind {
......@@ -237,12 +236,14 @@ func constructKnowledgeMapRenderAssignment(
valKnowledgeMap.assigned = append(valKnowledgeMap.assigned, expr.right)
valKnowledgeMap.creator = append(valKnowledgeMap.creator, blck.principal.name)
valKnowledgeMap.knownBy = append(valKnowledgeMap.knownBy, []map[string]string{{}})
valKnowledgeMap.phase = append(valKnowledgeMap.phase, phase)
valKnowledgeMap.phase = append(valKnowledgeMap.phase, []int{})
}
return valKnowledgeMap
}
func constructKnowledgeMapRenderMessage(valKnowledgeMap knowledgeMap, blck block) knowledgeMap {
func constructKnowledgeMapRenderMessage(
valKnowledgeMap knowledgeMap, blck block, currentPhase int,
) knowledgeMap {
for _, c := range blck.message.constants {
i := sanityGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
if i < 0 {
......@@ -252,7 +253,6 @@ func constructKnowledgeMapRenderMessage(valKnowledgeMap knowledgeMap, blck block
blck.message.recipient,
prettyConstant(c),
))
continue
}
c = valKnowledgeMap.constants[i]
senderKnows := false
......@@ -286,12 +286,12 @@ func constructKnowledgeMapRenderMessage(valKnowledgeMap knowledgeMap, blck block
blck.message.recipient,
prettyConstant(c),
))
default:
valKnowledgeMap.knownBy[i] = append(
valKnowledgeMap.knownBy[i],
map[string]string{blck.message.recipient: blck.message.sender},
)
}
valKnowledgeMap.knownBy[i] = append(
valKnowledgeMap.knownBy[i],
map[string]string{blck.message.recipient: blck.message.sender},
)
valKnowledgeMap.phase[i], _ = appendUniqueInt(valKnowledgeMap.phase[i], currentPhase)
}
return valKnowledgeMap
}
......@@ -312,7 +312,7 @@ func constructPrincipalStates(m Model, valKnowledgeMap knowledgeMap) []principal
beforeRewrite: []value{},
wasMutated: []bool{},
beforeMutate: []value{},
phase: []int{},
phase: [][]int{},
lock: 0,
}
for i, c := range valKnowledgeMap.constants {
......@@ -373,7 +373,7 @@ func constructPrincipalStateClone(valPrincipalState principalState, purify bool)
beforeRewrite: make([]value, len(valPrincipalState.beforeRewrite)),
wasMutated: make([]bool, len(valPrincipalState.wasMutated)),
beforeMutate: make([]value, len(valPrincipalState.beforeMutate)),
phase: make([]int, len(valPrincipalState.phase)),
phase: make([][]int, len(valPrincipalState.phase)),
lock: valPrincipalState.lock,
}
copy(valPrincipalStateClone.constants, valPrincipalState.constants)
......
......@@ -43,6 +43,9 @@ func replacementMapInit(valPrincipalState principalState, valAttackerState attac
if !valPrincipalState.known[ii] {
continue
}
if !intInSlice(valAttackerState.currentPhase, valPrincipalState.phase[ii]) {
continue
}
a := valPrincipalState.assigned[ii]
replacementsGroup.Add(1)
go func(v value) {
......
......@@ -26,6 +26,8 @@ func sanityPhases(m Model) {
switch blck.kind {
case "phase":
switch {
case m.attacker == "passive":
errorCritical("phases may only be used for analysis with an active attacker")
case blck.phase.number <= phase:
errorCritical(fmt.Sprintf(
"phase being declared (%d) must be superior to last declared phase (%d)",
......@@ -255,7 +257,7 @@ func sanityDeclaredPrincipals(m Model) []string {
for _, block := range m.blocks {
switch block.kind {
case "principal":
principals, _ = appendUnique(principals, block.principal.name)
principals, _ = appendUniqueString(principals, block.principal.name)
case "message":
if !strInSlice(block.message.sender, principals) {
errorCritical(fmt.Sprintf(
......
......@@ -85,7 +85,8 @@ type knowledgeMap struct {
assigned []value
creator []string
knownBy [][]map[string]string
phase []int
phase [][]int
maxPhase int
unnamedCounter int
}
......@@ -146,15 +147,16 @@ type principalState struct {
beforeRewrite []value
wasMutated []bool
beforeMutate []value
phase []int
phase [][]int
lock int
}
type attackerState struct {
active bool
known []value
wire []bool
mutatedTo [][]string
active bool
currentPhase int
known []value
wire []bool
mutatedTo [][]string
}
type attackerStateWrite struct {
......
......@@ -9,6 +9,7 @@ import (
"fmt"
"os"
"runtime"
"sort"
"github.com/logrusorgru/aurora"
)
......@@ -30,14 +31,41 @@ func strInSlice(x string, a []string) bool {
return false
}
// appendUnique appends a string to a slice only if it is unique within that slice.
func appendUnique(a []string, x string) ([]string, error) {
// intInSlice checks if an integer can be found within a slice.
func intInSlice(x int, a []int) bool {
for _, n := range a {
if x == n {
return true
}
}
return false
}
// appendUniqueString appends a string to a slice only if it is unique within that slice.
func appendUniqueString(a []string, x string) ([]string, error) {
if !strInSlice(x, a) {
return append(a, x), nil
}
return a, errors.New("string is not unique")
}
// appendUniqueInt appends an integer to a slice only if it is unique within that slice.
func appendUniqueInt(a []int, x int) ([]int, error) {
if !intInSlice(x, a) {
return append(a, x), nil
}
return a, errors.New("int is not unique")
}
// minIntInSlice returns the smallest integer in a slice of integers.
func minIntInSlice(v []int) (int, error) {
if len(v) == 0 {
return 0, errors.New("slice has no integers")
}
sort.Ints(v)
return v[0], nil
}
// colorOutputSupport tells us whether color output is supported based on the GOOS build target.
func colorOutputSupport() bool {
if runtime.GOOS == "windows" {
......
......@@ -15,16 +15,15 @@ import (
func Verify(filePath string) {
m, valKnowledgeMap, valPrincipalStates := parserParseModel(filePath)
initiated := time.Now().Format("03:04:05 PM")
attackerStateInit(m, valKnowledgeMap, m.attacker == "active")
verifyResultsInit(m)
prettyMessage(fmt.Sprintf(
"Verification initiated for '%s' at %s.", m.fileName, initiated,
), "verifpal", false)
switch m.attacker {
case "passive":
verifyPassive(valKnowledgeMap, valPrincipalStates)
verifyPassive(m, valKnowledgeMap, valPrincipalStates)
case "active":
verifyActive(valKnowledgeMap, valPrincipalStates)
verifyActive(m, valKnowledgeMap, valPrincipalStates)
default:
errorCritical(fmt.Sprintf("invalid attacker (%s)", m.attacker))
}
......@@ -58,15 +57,19 @@ func verifyStandardRun(valKnowledgeMap knowledgeMap, valPrincipalStates []princi
}
}
func verifyPassive(valKnowledgeMap knowledgeMap, valPrincipalStates []principalState) {
func verifyPassive(m Model, valKnowledgeMap knowledgeMap, valPrincipalStates []principalState) {
prettyMessage("Attacker is configured as passive.", "info", false)
attackerStateInit(false)
attackerStatePutPhaseUpdate(m, valKnowledgeMap, 0)
verifyStandardRun(valKnowledgeMap, valPrincipalStates, 0)
}
func verifyEnd() {
exitCode := 0
valVerifyResults, fileName := verifyResultsGetRead()
for _, verifyResult := range valVerifyResults {
if verifyResult.resolved {
exitCode = 1
prettyMessage(fmt.Sprintf(
"%s: %s",
prettyQuery(verifyResult.query),
......@@ -79,5 +82,5 @@ func verifyEnd() {
"Verification completed for '%s' at %s.", fileName, completed,
), "verifpal", false)
prettyMessage("Thank you for using Verifpal.", "verifpal", false)
os.Exit(0)
os.Exit(exitCode)
}
......@@ -5,15 +5,21 @@
package verifpal
import (
"fmt"
"sync"
)
func verifyActive(valKnowledgeMap knowledgeMap, valPrincipalStates []principalState) {
func verifyActive(m Model, valKnowledgeMap knowledgeMap, valPrincipalStates []principalState) {
prettyMessage("Attacker is configured as active.", "info", false)
verifyStandardRun(valKnowledgeMap, valPrincipalStates, 0)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 1)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 2)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 3)
for phase := 0; phase <= valKnowledgeMap.maxPhase; phase++ {
prettyMessage(fmt.Sprintf("Running at phase %d.", phase), "info", false)
attackerStateInit(true)
attackerStatePutPhaseUpdate(m, valKnowledgeMap, phase)
verifyStandardRun(valKnowledgeMap, valPrincipalStates, 0)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 1)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 2)
verifyActiveStages(valKnowledgeMap, valPrincipalStates, 3)
}
}
func verifyActiveStages(valKnowledgeMap knowledgeMap, valPrincipalStates []principalState, stage int) {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment