From 221b85db613c6634069f323f84d21c89454db6db Mon Sep 17 00:00:00 2001 From: Nadim Kobeissi Date: Wed, 29 Jan 2020 18:24:03 +0100 Subject: [PATCH] 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 (ad26547) and those extensions will be pushed onto their respective marketplaces shortly. The Verifpal User Manual will also be updated. --- examples/scuttlebutt_handshake.vp | 2 +- examples/signal.vp | 5 +++ examples/signal_small.vp | 9 +++- internal/verifpal/attackerstate.go | 65 +++++++++++++++++++---------- internal/verifpal/construct.go | 54 ++++++++++++------------ internal/verifpal/replacementmap.go | 3 ++ internal/verifpal/sanity.go | 4 +- internal/verifpal/types.go | 14 ++++--- internal/verifpal/util.go | 32 +++++++++++++- internal/verifpal/verify.go | 13 +++--- internal/verifpal/verifyactive.go | 16 ++++--- 11 files changed, 147 insertions(+), 70 deletions(-) diff --git a/examples/scuttlebutt_handshake.vp b/examples/scuttlebutt_handshake.vp index bc2d6d8..d2eaf77 100644 --- a/examples/scuttlebutt_handshake.vp +++ b/examples/scuttlebutt_handshake.vp @@ -3,7 +3,7 @@ attacker[active] -// Setup phase +// Setup principal Alice[ knows public n diff --git a/examples/signal.vp b/examples/signal.vp index b5f3c70..f84d4fe 100644 --- a/examples/signal.vp +++ b/examples/signal.vp @@ -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 diff --git a/examples/signal_small.vp b/examples/signal_small.vp index 939654c..0def040 100644 --- a/examples/signal_small.vp +++ b/examples/signal_small.vp @@ -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 diff --git a/internal/verifpal/attackerstate.go b/internal/verifpal/attackerstate.go index 2e4ab65..f36cda0 100644 --- a/internal/verifpal/attackerstate.go +++ b/internal/verifpal/attackerstate.go @@ -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) +} diff --git a/internal/verifpal/construct.go b/internal/verifpal/construct.go index f300a18..1190641 100644 --- a/internal/verifpal/construct.go +++ b/internal/verifpal/construct.go @@ -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) diff --git a/internal/verifpal/replacementmap.go b/internal/verifpal/replacementmap.go index e85e5e9..3c470c6 100644 --- a/internal/verifpal/replacementmap.go +++ b/internal/verifpal/replacementmap.go @@ -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) { diff --git a/internal/verifpal/sanity.go b/internal/verifpal/sanity.go index d8b59c8..6b6fb57 100644 --- a/internal/verifpal/sanity.go +++ b/internal/verifpal/sanity.go @@ -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( diff --git a/internal/verifpal/types.go b/internal/verifpal/types.go index 17d67c9..d06ddbf 100644 --- a/internal/verifpal/types.go +++ b/internal/verifpal/types.go @@ -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 { diff --git a/internal/verifpal/util.go b/internal/verifpal/util.go index c05418e..b438f0f 100644 --- a/internal/verifpal/util.go +++ b/internal/verifpal/util.go @@ -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" { diff --git a/internal/verifpal/verify.go b/internal/verifpal/verify.go index d1c0ee0..2569856 100644 --- a/internal/verifpal/verify.go +++ b/internal/verifpal/verify.go @@ -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) } diff --git a/internal/verifpal/verifyactive.go b/internal/verifpal/verifyactive.go index d66a1c3..ec4dbc1 100644 --- a/internal/verifpal/verifyactive.go +++ b/internal/verifpal/verifyactive.go @@ -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) { -- GitLab