Verified Commit 1613a48c authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Analysis tweaks and fixes

parent 7d1e8362
Pipeline #613 passed with stages
in 1 minute and 54 seconds
......@@ -235,6 +235,10 @@ var verifpalTests = []VerifpalTest{
Model: "ffgg.vp",
ResultsCode: "c1",
},
{
Model: "exa.vp",
ResultsCode: "c1",
},
}
func TestMain(t *testing.T) {
......
......@@ -6,15 +6,12 @@ package vplogic
import (
"fmt"
"sync"
)
func mutationMapInit(
valKnowledgeMap KnowledgeMap, valPrincipalState PrincipalState,
valAttackerState AttackerState, stage int,
) (MutationMap, error) {
var mutationMapGroup sync.WaitGroup
var mutationMapMutex sync.Mutex
var err error
valMutationMap := MutationMap{
Initialized: true,
......@@ -28,44 +25,28 @@ func mutationMapInit(
"Initializing Stage %d mutation map for %s...", stage, valPrincipalState.Name,
), "analysis", false)
for _, v := range valAttackerState.Known {
mutationMapGroup.Add(1)
go func(v Value, valKnowledgeMap KnowledgeMap,
valPrincipalState PrincipalState, valAttackerState AttackerState,
) {
switch v.Kind {
case "primitive":
mutationMapGroup.Done()
return
case "equation":
mutationMapGroup.Done()
return
}
a, i := valueResolveConstant(v.Constant, valPrincipalState)
if mutationMapSkipValue(v, i, valKnowledgeMap, valPrincipalState, valAttackerState) {
mutationMapGroup.Done()
return
}
var c Constant
var r []Value
c, r, err = mutationMapReplaceValue(
a, v, i, stage, valPrincipalState, valAttackerState,
)
if err != nil {
mutationMapGroup.Done()
return
}
if len(r) == 0 {
mutationMapGroup.Done()
return
}
mutationMapMutex.Lock()
valMutationMap.Constants = append(valMutationMap.Constants, c)
valMutationMap.Mutations = append(valMutationMap.Mutations, r)
mutationMapMutex.Unlock()
mutationMapGroup.Done()
}(v, valKnowledgeMap, valPrincipalState, valAttackerState)
switch v.Kind {
case "primitive":
continue
case "equation":
continue
}
a, i := valueResolveConstant(v.Constant, valPrincipalState)
if mutationMapSkipValue(v, i, valKnowledgeMap, valPrincipalState, valAttackerState) {
continue
}
var c Constant
var r []Value
c, r, err = mutationMapReplaceValue(
a, v, i, stage, valPrincipalState, valAttackerState,
)
if len(r) == 0 {
continue
}
valMutationMap.Constants = append(valMutationMap.Constants, c)
valMutationMap.Mutations = append(valMutationMap.Mutations, r)
}
mutationMapGroup.Wait()
valMutationMap.Combination = make([]Value, len(valMutationMap.Constants))
valMutationMap.DepthIndex = make([]int, len(valMutationMap.Constants))
for iiii := range valMutationMap.Constants {
......@@ -81,16 +62,12 @@ func mutationMapSkipValue(
switch {
case i < 0:
return true
case !strInSlice(valPrincipalState.Name, valPrincipalState.Wire[i]):
return true
case valPrincipalState.Guard[i]:
if !strInSlice(valPrincipalState.Sender[i], valPrincipalState.MutatableTo[i]) {
return true
}
case valPrincipalState.Creator[i] == valPrincipalState.Name:
return true
case !valPrincipalState.Known[i]:
return true
case !valueConstantIsUsedByPrincipalInKnowledgeMap(valKnowledgeMap, valPrincipalState.Name, v.Constant):
return true
case !intInSlice(valAttackerState.CurrentPhase, valPrincipalState.Phase[i]):
......
......@@ -55,7 +55,7 @@ func queryConfidentiality(
written := verifyResultsPutWrite(result)
if written {
InfoMessage(fmt.Sprintf(
"%s: %s", prettyQuery(query), result.Summary,
"%s %s", prettyQuery(query), result.Summary,
), "result", true)
}
return result
......@@ -175,7 +175,7 @@ func queryAuthenticationHandlePass(
written := verifyResultsPutWrite(result)
if written {
InfoMessage(fmt.Sprintf(
"%s: %s", prettyQuery(result.Query), result.Summary,
"%s %s", prettyQuery(result.Query), result.Summary,
), "result", true)
}
return result
......@@ -212,7 +212,7 @@ func queryFreshness(
written := verifyResultsPutWrite(result)
if written {
InfoMessage(fmt.Sprintf(
"%s: %s", prettyQuery(query), result.Summary,
"%s %s", prettyQuery(query), result.Summary,
), "result", true)
}
return result, nil
......@@ -261,7 +261,7 @@ func queryUnlinkability(
written := verifyResultsPutWrite(result)
if written {
InfoMessage(fmt.Sprintf(
"%s: %s", prettyQuery(query), result.Summary,
"%s %s", prettyQuery(query), result.Summary,
), "result", true)
}
return result, nil
......@@ -303,7 +303,7 @@ func queryUnlinkability(
written := verifyResultsPutWrite(result)
if written {
InfoMessage(fmt.Sprintf(
"%s: %s", prettyQuery(query), result.Summary,
"%s %s", prettyQuery(query), result.Summary,
), "result", true)
}
return result, nil
......
......@@ -633,13 +633,15 @@ func valueResolveValueInternalValuesFromPrincipalState(
forceBeforeMutate = true
}
}
if !forceBeforeMutate {
if forceBeforeMutate {
forceBeforeMutate = !strInSlice(valPrincipalState.Creator[rootIndex], valPrincipalState.MutatableTo[nextRootIndex])
} else {
forceBeforeMutate = valueShouldResolveToBeforeMutate(nextRootIndex, valPrincipalState)
}
if forceBeforeMutate {
a = valPrincipalState.BeforeMutate[nextRootIndex]
} else {
a, _ = valueResolveConstant(a.Constant, valPrincipalState)
a = valPrincipalState.Assigned[nextRootIndex]
}
rootIndex = nextRootIndex
rootValue = a
......@@ -773,15 +775,15 @@ func valueResolveAllPrincipalStateValues(
valPrincipalStateClone := constructPrincipalStateClone(valPrincipalState, false)
for i := range valPrincipalState.Assigned {
valPrincipalStateClone.Assigned[i], err = valueResolveValueInternalValuesFromPrincipalState(
valPrincipalState.Assigned[i], valPrincipalState.Assigned[i], i, valPrincipalState, valAttackerState,
valueShouldResolveToBeforeMutate(i, valPrincipalState), 0,
valPrincipalState.Assigned[i], valPrincipalState.Assigned[i], i, valPrincipalState,
valAttackerState, valueShouldResolveToBeforeMutate(i, valPrincipalState), 0,
)
if err != nil {
return PrincipalState{}, err
}
valPrincipalStateClone.BeforeRewrite[i], err = valueResolveValueInternalValuesFromPrincipalState(
valPrincipalState.BeforeRewrite[i], valPrincipalState.BeforeRewrite[i], i, valPrincipalState, valAttackerState,
valueShouldResolveToBeforeMutate(i, valPrincipalState), 0,
valPrincipalState.BeforeRewrite[i], valPrincipalState.BeforeRewrite[i], i, valPrincipalState,
valAttackerState, valueShouldResolveToBeforeMutate(i, valPrincipalState), 0,
)
if err != nil {
return PrincipalState{}, err
......
......@@ -157,7 +157,7 @@ func verifyEnd(m Model) ([]VerifyResult, string, error) {
for _, verifyResult := range valVerifyResults {
if verifyResult.Resolved {
InfoMessage(fmt.Sprintf(
"%s: %s",
"%s %s",
prettyQuery(verifyResult.Query),
verifyResult.Summary,
), "result", false)
......
......@@ -118,8 +118,7 @@ func verifyActiveScan(
}
func verifyActiveMutatePrincipalState(
valPrincipalState PrincipalState,
valAttackerState AttackerState, valMutationMap MutationMap,
valPrincipalState PrincipalState, valAttackerState AttackerState, valMutationMap MutationMap,
) (PrincipalState, bool, error) {
isWorthwhileMutation := false
for i, c := range valMutationMap.Constants {
......
// SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal P1[
knows private k1
knows private M
knows public c
key = AEAD_ENC(k1, c, c)
// AEAD_ENC(AEAD_ENC(k1, c, c), m, c)
msg1 = AEAD_ENC(key, M, c)
msg3 = AEAD_ENC(AEAD_ENC(k1,msg1,c),c,c)
]
P1 -> P2: msg1
principal P2[
knows private k1
knows private k2
knows public c
msg2 = AEAD_ENC(k2,AEAD_ENC(k1,msg1,c),c)
]
P2 -> P3: [msg2]
P1 -> P3: msg3
principal P3[
knows private k2
knows public c
clear = AEAD_DEC(k2,msg2,c)?
msg4 = AEAD_DEC(clear,msg3,c)?
]
P3 -> P1: [msg4]
queries[
confidentiality? M
]
\ No newline at end of file
......@@ -25,14 +25,14 @@ Bob -> Carol: [gb]
Carol -> Alice: [gc]
Carol -> Bob: [gc]
principal Bob[
principal Alice[
knows private m
sb = RINGSIGN(b, ga, gc, m)
sa = RINGSIGN(a, gb, gc, m)
]
principal Alice[
principal Bob[
knows private m
sa = RINGSIGN(a, gb, gc, m)
sb = RINGSIGN(b, ga, gc, m)
]
principal Carol[
......@@ -40,11 +40,11 @@ principal Carol[
sc = RINGSIGN(c, ga, gb, m)
]
Alice -> Damian: [sa]
Alice -> Damian: [ga], [sa]
Carol -> Damian: [sc]
Bob -> Damian: [gb], m, sb
Bob -> Damian: [ga], [gb], [gc], m, sb
Carol -> Damian: [gc], [sc]
principal Damian[
_ = RINGSIGNVERIF(ga, gb, gc, m, sb)?
......
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