diff --git a/examples/scuttlebutt_handshake.vp b/examples/scuttlebutt_handshake.vp index bc2d6d87834ad2172adcdf72122e9642979175b4..d2eaf77869efc6a017423956e88034ed1ba4db90 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 b5f3c70906c5427c1614bee2be1794fe84949a41..f84d4fe55650d394d7fa3dcf64a719b7416b690d 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 939654ce50e4485cf82814848f25c8f17704667a..0def0409fe32dc345f48c0f79089d780c80d214f 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 2e4ab65180246777e3703444e8ed458423ed077e..f36cda03814b3d81dd09052fbbc5006e6b57ea17 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 f300a18b309c01b8bdae1001c3a68303205b4d3c..1190641236860d0c0ba0578cf13410670586b0e1 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 e85e5e9cdbe9a021caad5e478679b106269b985e..3c470c6d9647449f8f6ffa6f37785ea202928adb 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 d8b59c81282c291d14fa1a67a5a80dd334c29d3d..6b6fb575d259da441b805acae4a25b17c5f7d90c 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 17d67c9fa6a7aefaaf74e6c7c92bbf8914ed7e55..d06ddbf904229e962cdda24ed7ee36e7978efa78 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 c05418eb20222d0b6a29039637783bd79b7d4176..b438f0f185f775ee576a19231e7423aff5893301 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 d1c0ee0edebbeefc64606a1a8521646573a4326c..2569856a5436200ba4833b2349314f827b9735a0 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 d66a1c3dea02438f40b354158e201d97393ba180..ec4dbc10424912119eb8c90efc178545e79ddebf 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) {