Commit 672c4220 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Minor fixes and cleanup

parent e8baab21
Pipeline #636 passed with stages
in 1 minute and 54 seconds
......@@ -91,6 +91,8 @@ linters-settings:
statements: 64
lines: 128
gocyclo:
min-complexity: 20
min-complexity: 15
govet:
enable-all: true
lll:
line-length: 120
\ No newline at end of file
......@@ -89,7 +89,7 @@ func coqBlockByPhase(valKnowledgeMap KnowledgeMap, phase []Block, output []strin
for _, block := range phase {
switch block.Kind {
case "principal":
cpb, err = coqPrincipalBlock(block, valKnowledgeMap)
cpb, err = coqPrincipal(block, valKnowledgeMap)
if err != nil {
return []string{}, err
}
......@@ -127,7 +127,8 @@ func coqPrincipalNames(principals []string) string {
return output + "]."
}
func coqPrincipalBlock(block Block, valKnowledgeMap KnowledgeMap) (string, error) {
func coqPrincipal(block Block, valKnowledgeMap KnowledgeMap) (string, error) {
var err error
expressions := []string{""}
for i, expression := range block.Principal.Expressions {
switch expression.Kind {
......@@ -142,10 +143,8 @@ func coqPrincipalBlock(block Block, valKnowledgeMap KnowledgeMap) (string, error
}
default:
for _, c := range expression.Constants {
crc, err := coqResolveConstant(c, valKnowledgeMap)
if err != nil {
return "", err
}
var crc string
crc, err = coqResolveConstant(c, valKnowledgeMap)
expressions = append(expressions, fmt.Sprintf(
"EXP knowledge %s %s unleaked;",
expression.Qualifier, crc,
......@@ -154,29 +153,23 @@ func coqPrincipalBlock(block Block, valKnowledgeMap KnowledgeMap) (string, error
}
case "generates":
for _, c := range expression.Constants {
crv, err := coqResolveConstant(c, valKnowledgeMap)
if err != nil {
return "", err
}
var crv string
crv, err = coqResolveConstant(c, valKnowledgeMap)
expressions = append(expressions, fmt.Sprintf(
"EXP generation private %s unleaked;", crv,
))
}
case "leaks":
for _, c := range expression.Constants {
crc, err := coqResolveConstant(c, valKnowledgeMap)
if err != nil {
return "", err
}
var crc string
crc, err = coqResolveConstant(c, valKnowledgeMap)
expressions = append(expressions, fmt.Sprintf(
"EXP knows public %s leaked;", crc,
))
}
case "assignment":
cae, err := coqAssignemntExpression(expression, valKnowledgeMap)
if err != nil {
return "", err
}
var cae []string
cae, err = coqAssignemntExpression(expression, valKnowledgeMap)
expressions = append(expressions, cae...)
}
if len(block.Principal.Expressions) == i+1 {
......@@ -185,6 +178,9 @@ func coqPrincipalBlock(block Block, valKnowledgeMap KnowledgeMap) (string, error
)
expressions = append(expressions, "")
}
if err != nil {
return "", err
}
}
return strings.Join(expressions, "\n\t\t\t\t"), nil
}
......
......@@ -221,13 +221,11 @@ func infoQueryMutatedValues(
mutated := []Value{}
targetInfo := "In another session:"
mutatedInfo := ""
relevant := false
for i, a := range valPrincipalState.BeforeRewrite {
if valueEquivalentValues(a, valKnowledgeMap.Assigned[i], false) {
continue
}
pc := prettyConstant(valPrincipalState.Constants[i])
pa := prettyValue(valPrincipalState.Assigned[i])
pn := make([]string, 4)
isTargetValue := valueEquivalentValues(
targetValue, valPrincipalState.Assigned[i], false,
)
......@@ -248,49 +246,77 @@ func infoQueryMutatedValues(
mutated = append(mutated, valPrincipalState.Assigned[i])
}
}
if colorOutputSupport() {
pn[0] = aurora.BrightYellow(pc).Italic().String()
pn[1] = aurora.BrightYellow(" → ").Italic().String()
pn[2] = aurora.BrightYellow(pa).Italic().String()
pn[3] = ""
if isTargetValue && !valPrincipalState.Mutated[i] {
pn[0] = aurora.BrightYellow(pc).Italic().Underline().String()
pn[1] = aurora.BrightYellow(" → ").Italic().Underline().String()
pn[2] = aurora.BrightYellow(pa).Italic().Underline().String()
pn[3] = aurora.Red("← obtained by Attacker").Italic().String()
} else if valPrincipalState.Mutated[i] {
pn[3] = aurora.Red(
fmt.Sprintf("← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[i]),
),
).Italic().String()
}
} else {
pn[0] = pc
pn[1] = " → "
pn[2] = pa
pn[3] = ""
if isTargetValue && !valPrincipalState.Mutated[i] {
pn[3] = "← obtained by Attacker"
} else if valPrincipalState.Mutated[i] {
pn[3] = fmt.Sprintf("← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[i]),
)
}
}
mutatedInfo = fmt.Sprintf("%s\n %s%s%s %s",
mutatedInfo, pn[0], pn[1], pn[2], pn[3],
mInfo, mRelevant := infoQueryMutatedValue(
valKnowledgeMap, valPrincipalState, i, isTargetValue,
)
if mRelevant {
relevant = true
}
mutatedInfo = fmt.Sprintf("%s\n %s", mutatedInfo, mInfo)
}
if !relevant {
return ""
}
for _, m := range mutated {
ai := valueEquivalentValueInValues(m, valAttackerState.Known)
if ai < 0 {
continue
}
mmInfo := infoQueryMutatedValues(valKnowledgeMap, valAttackerState.PrincipalState[ai], valAttackerState, m)
mmInfo := infoQueryMutatedValues(
valKnowledgeMap, valAttackerState.PrincipalState[ai],
valAttackerState, m,
)
if len(mmInfo) > 0 {
mutatedInfo = fmt.Sprintf("%s\n\n %s%s", mmInfo, targetInfo, mutatedInfo)
mutatedInfo = fmt.Sprintf(
"%s\n\n %s%s",
mmInfo, targetInfo, mutatedInfo,
)
}
}
return mutatedInfo
}
func infoQueryMutatedValue(
valKnowledgeMap KnowledgeMap, valPrincipalState PrincipalState,
index int, isTargetValue bool,
) (string, bool) {
pc := prettyConstant(valPrincipalState.Constants[index])
pa := prettyValue(valPrincipalState.Assigned[index])
relevant := false
pn := make([]string, 4)
if colorOutputSupport() {
pn[0] = aurora.BrightYellow(pc).Italic().String()
pn[1] = aurora.BrightYellow(" → ").Italic().String()
pn[2] = aurora.BrightYellow(pa).Italic().String()
pn[3] = ""
if isTargetValue && !valPrincipalState.Mutated[index] {
relevant = true
pn[0] = aurora.BrightYellow(pc).Italic().Underline().String()
pn[1] = aurora.BrightYellow(" → ").Italic().Underline().String()
pn[2] = aurora.BrightYellow(pa).Italic().Underline().String()
pn[3] = aurora.Red(" ← obtained by Attacker").Italic().String()
} else if valPrincipalState.Mutated[index] {
relevant = true
pn[3] = aurora.Red(
fmt.Sprintf(" ← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[index]),
),
).Italic().String()
}
} else {
pn[0] = pc
pn[1] = " → "
pn[2] = pa
pn[3] = ""
if isTargetValue && !valPrincipalState.Mutated[index] {
relevant = true
pn[3] = " ← obtained by Attacker"
} else if valPrincipalState.Mutated[index] {
relevant = true
pn[3] = fmt.Sprintf(" ← mutated by Attacker (originally %s)",
prettyValue(valKnowledgeMap.Assigned[index]),
)
}
}
return strings.Join(pn, ""), relevant
}
......@@ -214,16 +214,10 @@ func injectPrimitive(
kinjectants[arg] = append(kinjectants[arg], k)
}
if stage >= 5 && injectDepth <= stage-5 {
kp := inject(
k.Primitive, injectDepth+1,
valPrincipalState, valAttackerState, stage,
uinjectants, kinjectants = injectPrimitiveRecursively(
k, arg, uinjectants, kinjectants,
valPrincipalState, valAttackerState, injectDepth, stage,
)
for _, kkp := range kp {
if valueEquivalentValueInValues(kkp, uinjectants[arg]) < 0 {
uinjectants[arg] = append(uinjectants[arg], kkp)
kinjectants[arg] = append(kinjectants[arg], kkp)
}
}
}
case "equation":
if valueEquivalentValueInValues(k, uinjectants[arg]) < 0 {
......@@ -236,6 +230,24 @@ func injectPrimitive(
return injectLoopN(p, kinjectants)
}
func injectPrimitiveRecursively(
k Value, arg int, uinjectants [][]Value, kinjectants [][]Value,
valPrincipalState PrincipalState, valAttackerState AttackerState,
injectDepth int, stage int,
) ([][]Value, [][]Value) {
kp := inject(
k.Primitive, injectDepth+1,
valPrincipalState, valAttackerState, stage,
)
for _, kkp := range kp {
if valueEquivalentValueInValues(kkp, uinjectants[arg]) < 0 {
uinjectants[arg] = append(uinjectants[arg], kkp)
kinjectants[arg] = append(kinjectants[arg], kkp)
}
}
return uinjectants, kinjectants
}
func injectLoopN(p Primitive, kinjectants [][]Value) []Value {
if verifyResultsAllResolved() {
return []Value{}
......
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