Skip to content

GitLab

Verifpal
Verifpal
Unverified Commit 7467e8ab authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎
Browse files
Options

New primitives: SHAMIR_SPLIT, SHAMIR_JOIN

parent c555a737
Hide whitespace changes
Inline Side-by-side
Showing with 346 additions and 129 deletions
internal/verifpal/possible.go
View file @ 7467e8ab
......@@ -8,18 +8,18 @@ import (
"fmt"
)
func possibleToDeconstructPrimitive(
func possibleToDecomposePrimitive(
p primitive, valAttackerState *attackerState, valPrincipalState *principalState,
analysis int, depth int,
) (bool, value, []value) {
has := []value{}
primitive := primitiveGet(p.name)
if !primitive.decompose.hasRule {
prim := primitiveGet(p.name)
if !prim.decompose.hasRule {
return false, value{}, has
}
for i, g := range primitive.decompose.given {
for i, g := range prim.decompose.given {
a := p.arguments[g]
a, valid := primitive.decompose.filter(a, i, valPrincipalState)
a, valid := prim.decompose.filter(a, i, valPrincipalState)
ii := sanityEquivalentValueInValues(a, &valAttackerState.known, valPrincipalState)
if valid && ii >= 0 {
has = append(has, a)
......@@ -32,7 +32,7 @@ func possibleToDeconstructPrimitive(
has = append(has, a)
continue
}
r, _, _ = possibleToDeconstructPrimitive(a.primitive, valAttackerState, valPrincipalState, analysis, depth)
r, _, _ = possibleToDecomposePrimitive(a.primitive, valAttackerState, valPrincipalState, analysis, depth)
if r {
has = append(has, a)
continue
......@@ -45,12 +45,12 @@ func possibleToDeconstructPrimitive(
}
}
}
if len(has) >= len(primitive.decompose.given) {
revealed := p.arguments[primitive.decompose.reveal]
if len(has) >= len(prim.decompose.given) {
revealed := p.arguments[prim.decompose.reveal]
if sanityExactSameValueInValues(revealed, &valAttackerState.known) < 0 {
if sanityExactSameValueInValues(revealed, &valAttackerState.conceivable) < 0 {
prettyMessage(fmt.Sprintf(
"%s now conceivable by deconstructing %s with %s.",
"%s now conceivable by decomposing %s with %s.",
prettyValue(revealed), prettyPrimitive(p), prettyValues(has),
), analysis, depth, "analysis")
valAttackerState.conceivable = append(valAttackerState.conceivable, revealed)
......@@ -64,14 +64,48 @@ func possibleToDeconstructPrimitive(
return false, value{}, has
}
func possibleToRecomposePrimitive(
p primitive, valAttackerState *attackerState, valPrincipalState *principalState,
analysis int, depth int,
) (bool, value, []value) {
prim := primitiveGet(p.name)
if !prim.recompose.hasRule {
return false, value{}, []value{}
}
for _, i := range prim.recompose.given {
ar := []value{}
for _, ii := range i {
for _, v := range valAttackerState.known {
vb := v
switch v.kind {
case "constant":
v = sanityResolveConstant(v.constant, valPrincipalState, false)
}
switch v.kind {
case "constant":
continue
case "primitive":
equivPrim, vo, _ := sanityEquivalentPrimitives(v.primitive, p, valPrincipalState, false)
if equivPrim && vo == ii {
ar = append(ar, vb)
if len(ar) >= len(i) {
return true, p.arguments[prim.recompose.reveal], ar
}
}
case "equation":
continue
}
}
}
}
return false, value{}, []value{}
}
func possibleToReconstructPrimitive(
p primitive, valAttackerState *attackerState, valPrincipalState *principalState,
analysis int, depth int,
) (bool, []value) {
d, _, has := possibleToDeconstructPrimitive(p, valAttackerState, valPrincipalState, analysis, depth)
if d {
return true, has
}
has := []value{}
for _, a := range p.arguments {
if sanityEquivalentValueInValues(a, &valAttackerState.known, valPrincipalState) >= 0 {
has = append(has, a)
......@@ -79,7 +113,7 @@ func possibleToReconstructPrimitive(
}
switch a.kind {
case "primitive":
r, _, _ := possibleToDeconstructPrimitive(a.primitive, valAttackerState, valPrincipalState, analysis, depth)
r, _, _ := possibleToDecomposePrimitive(a.primitive, valAttackerState, valPrincipalState, analysis, depth)
if r {
has = append(has, a)
continue
......@@ -123,7 +157,7 @@ func possibleToReconstructEquation(
e equation,
valAttackerState *attackerState, valPrincipalState *principalState,
) (bool, []value) {
eValues := sanityDeconstructEquationValues(e, valPrincipalState)
eValues := sanityDecomposeEquationValues(e, valPrincipalState)
if len(eValues) > 2 {
i := sanityGetPrincipalStateIndexFromConstant(valPrincipalState, eValues[2].constant)
if i < 0 {
......@@ -170,7 +204,7 @@ func possibleToPassAssert(p primitive, valPrincipalState *principalState) (bool,
return false, value{kind: "primitive", primitive: p}
}
func possibleToPassRewrite(p primitive, valPrincipalState *principalState) (bool, value) {
func possibleToRewrite(p primitive, valPrincipalState *principalState) (bool, value) {
if p.name == "ASSERT" {
return possibleToPassAssert(p, valPrincipalState)
}
......@@ -204,17 +238,17 @@ func possibleToPassRewrite(p primitive, valPrincipalState *principalState) (bool
return true, rewrite
}
func possibleToForcePassRewrite(p primitive, valPrincipalState *principalState, valAttackerState *attackerState, analysis int, depth int) bool {
func possibleToForceRewrite(p primitive, valPrincipalState *principalState, valAttackerState *attackerState, analysis int, depth int) bool {
switch p.name {
case "DEC", "AEAD_DEC":
return possibleToForcePassRewriteDECandAEADDEC(p, valPrincipalState, valAttackerState, analysis, depth)
return possibleToForceRewriteDECandAEADDEC(p, valPrincipalState, valAttackerState, analysis, depth)
case "SIGNVERIF":
return possibleToForcePassRewriteSIGNVERIF(p, valPrincipalState, valAttackerState, analysis, depth)
return possibleToForceRewriteSIGNVERIF(p, valPrincipalState, valAttackerState, analysis, depth)
}
return false
}
func possibleToForcePassRewriteDECandAEADDEC(
func possibleToForceRewriteDECandAEADDEC(
p primitive, valPrincipalState *principalState, valAttackerState *attackerState,
analysis int, depth int,
) bool {
......@@ -239,7 +273,7 @@ func possibleToForcePassRewriteDECandAEADDEC(
return false
}
func possibleToForcePassRewriteSIGNVERIF(
func possibleToForceRewriteSIGNVERIF(
p primitive, valPrincipalState *principalState, valAttackerState *attackerState,
analysis int, depth int,
) bool {
......@@ -258,33 +292,43 @@ func possibleToForcePassRewriteSIGNVERIF(
return false
}
/*
func possibleToForcePassRewriteASSERT(
p primitive, valPrincipalState *principalState, valAttackerState *attackerState,
analysis int, depth int,
) bool {
for ii := range p.arguments {
iii := 0
if ii == 0 {
iii = 1
}
r := false
aii := p.arguments[ii]
aiii := p.arguments[iii]
r = sanityEquivalentValueInValues(aii, &valAttackerState.known, valPrincipalState) >= 0
if r && sanityEquivalentValues(aii, aiii, valPrincipalState) {
return true
}
switch aii.kind {
case "primitive":
r, _ = possibleToReconstructPrimitive(aii.primitive, valAttackerState, valPrincipalState, analysis, depth)
case "equation":
r, _ = possibleToReconstructEquation(aii.equation, valAttackerState, valPrincipalState)
}
if r && sanityEquivalentValues(aii, aiii, valPrincipalState) {
return true
func possibleToRebuild(p primitive, valPrincipalState *principalState) (bool, value) {
prim := primitiveGet(p.name)
if !prim.rebuild.hasRule {
return false, value{}
}
for _, i := range prim.rebuild.given {
has := []value{}
for _, ii := range i {
a := p.arguments[ii]
switch a.kind {
case "constant":
continue
case "primitive":
if a.primitive.name == prim.rebuild.name {
has = append(has, a)
}
case "equation":
continue
}
rebuildPasses := true
if len(has) >= len(i) {
for ai, aa := range has {
if ai == 0 {
continue
}
equivPrim, o1, o2 := sanityEquivalentPrimitives(has[0].primitive, aa.primitive, valPrincipalState, false)
if !equivPrim || (o1 == o2) {
rebuildPasses = false
}
}
} else {
rebuildPasses = false
}
if rebuildPasses {
return true, has[0].primitive.arguments[prim.rebuild.reveal]
}
}
}
return false
return false, value{}
}
*/
internal/verifpal/primitive.go
View file @ 7467e8ab
......@@ -14,9 +14,15 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -27,9 +33,15 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: false,
},
......@@ -45,9 +57,15 @@ var primitiveSpecs = []primitiveSpec{
return x, true
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -63,6 +81,9 @@ var primitiveSpecs = []primitiveSpec{
return x, true
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "AEAD_ENC",
......@@ -79,6 +100,9 @@ var primitiveSpecs = []primitiveSpec{
return x, false
},
},
rebuild: rebuildRule{
hasRule: false,
},
check: true,
injectable: false,
},
......@@ -94,9 +118,15 @@ var primitiveSpecs = []primitiveSpec{
return x, true
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -112,6 +142,9 @@ var primitiveSpecs = []primitiveSpec{
return x, true
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "ENC",
......@@ -126,6 +159,9 @@ var primitiveSpecs = []primitiveSpec{
return x, false
},
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: false,
},
......@@ -136,9 +172,15 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -149,10 +191,16 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
to: -1,
},
rebuild: rebuildRule{
hasRule: false,
},
check: true,
injectable: false,
},
......@@ -163,9 +211,15 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -176,6 +230,9 @@ var primitiveSpecs = []primitiveSpec{
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "SIGN",
......@@ -191,7 +248,7 @@ var primitiveSpecs = []primitiveSpec{
case "primitive":
return x, false
case "equation":
values := sanityDeconstructEquationValues(
values := sanityDecomposeEquationValues(
x.equation,
valPrincipalState,
)
......@@ -206,6 +263,9 @@ var primitiveSpecs = []primitiveSpec{
return x, false
},
},
rebuild: rebuildRule{
hasRule: false,
},
check: true,
injectable: false,
},
......@@ -226,7 +286,7 @@ var primitiveSpecs = []primitiveSpec{
case "primitive":
return x, false
case "equation":
values := sanityDeconstructEquationValues(
values := sanityDecomposeEquationValues(
x.equation,
valPrincipalState,
)
......@@ -241,9 +301,15 @@ var primitiveSpecs = []primitiveSpec{
return x, false
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
},
......@@ -259,6 +325,9 @@ var primitiveSpecs = []primitiveSpec{
return x, true
},
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "PKE_ENC",
......@@ -293,6 +362,69 @@ var primitiveSpecs = []primitiveSpec{
return x, false
},
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: false,
},
{
name: "SHAMIR_SPLIT",
arity: 1,
output: 3,
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: true,
given: [][]int{
[]int{0, 1},
[]int{0, 2},
[]int{1, 2},
},
reveal: 0,
filter: func(x value, i int, valPrincipalState *principalState) (value, bool) {
return x, true
},
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: false,
},
{
name: "SHAMIR_JOIN",
arity: 2,
output: 1,
decompose: decomposeRule{
hasRule: true,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: true,
name: "SHAMIR_SPLIT",
given: [][]int{
[]int{0, 1},
[]int{1, 0},
[]int{0, 2},
[]int{2, 0},
[]int{1, 2},
[]int{2, 1},
},
reveal: 0,
filter: func(x value, i int, valPrincipalState *principalState) (value, bool) {
return x, true
},
},
check: false,
injectable: false,
},
......
internal/verifpal/query.go
View file @ 7467e8ab
......@@ -73,8 +73,8 @@ func queryAuthentication(query query, valAttackerState *attackerState, valPrinci
continue
}
if primitiveGet(a.primitive.name).rewrite.hasRule {
pass, _ := possibleToPassRewrite(a.primitive, valPrincipalState)
forcedPass := possibleToForcePassRewrite(a.primitive, valPrincipalState, valAttackerState, 0, 0)
pass, _ := possibleToRewrite(a.primitive, valPrincipalState)
forcedPass := possibleToForceRewrite(a.primitive, valPrincipalState, valAttackerState, 0, 0)
if pass || forcedPass {
indices = append(indices, ii)
passes = append(passes, pass)
......
internal/verifpal/sanity.go
View file @ 7467e8ab
......@@ -44,16 +44,16 @@ func sanityAssignmentConstants(right value, constants []constant, valKnowledgeMa
}
func sanityAssignmentConstantsFromPrimitive(right value, constants []constant, valKnowledgeMap *knowledgeMap) []constant {
p := primitiveGet(right.primitive.name)
prim := primitiveGet(right.primitive.name)
if (len(right.primitive.arguments) == 0) ||
(len(right.primitive.arguments) > 5) ||
((p.arity >= 0) && (len(right.primitive.arguments) != p.arity)) {
((prim.arity >= 0) && (len(right.primitive.arguments) != prim.arity)) {
plural := ""
arity := fmt.Sprintf("%d", p.arity)
arity := fmt.Sprintf("%d", prim.arity)
if len(right.primitive.arguments) > 1 {
plural = "s"
}
if p.arity < 0 {
if prim.arity < 0 {
arity = "between 1 and 5"
}
errorCritical(fmt.Sprintf(
......@@ -273,7 +273,8 @@ func sanityEquivalentValues(a1 value, a2 value, valPrincipalState *principalStat
case "constant":
return false
case "primitive":
return sanityEquivalentPrimitives(a1.primitive, a2.primitive, valPrincipalState)
equivPrim, _, _ := sanityEquivalentPrimitives(a1.primitive, a2.primitive, valPrincipalState, true)
return equivPrim
case "equation":
return false
}
......@@ -290,28 +291,28 @@ func sanityEquivalentValues(a1 value, a2 value, valPrincipalState *principalStat
return true
}
func sanityEquivalentPrimitives(p1 primitive, p2 primitive, valPrincipalState *principalState) bool {
func sanityEquivalentPrimitives(p1 primitive, p2 primitive, valPrincipalState *principalState, considerOutput bool) (bool, int, int) {
if p1.name != p2.name {
return false
return false, 0, 0
}
if len(p1.arguments) != len(p2.arguments) {
return false
return false, 0, 0
}
if p1.output != p2.output {
return false
if considerOutput && (p1.output != p2.output) {
return false, 0, 0
}
for i := range p1.arguments {
equiv := sanityEquivalentValues(p1.arguments[i], p2.arguments[i], valPrincipalState)
if !equiv {
return false
return false, 0, 0
}
}
return true
return true, p1.output, p2.output
}
func sanityEquivalentEquations(e1 equation, e2 equation, valPrincipalState *principalState) bool {
e1Values := sanityDeconstructEquationValues(e1, valPrincipalState)
e2Values := sanityDeconstructEquationValues(e2, valPrincipalState)
e1Values := sanityDecomposeEquationValues(e1, valPrincipalState)
e2Values := sanityDecomposeEquationValues(e2, valPrincipalState)
if (len(e1Values) == 0) || (len(e2Values) == 0) {
return false
}
......@@ -319,8 +320,8 @@ func sanityEquivalentEquations(e1 equation, e2 equation, valPrincipalState *prin
return false
}
if e1Values[0].kind == "equation" && e2Values[0].kind == "equation" {
e1Base := sanityDeconstructEquationValues(e1Values[0].equation, valPrincipalState)
e2Base := sanityDeconstructEquationValues(e2Values[0].equation, valPrincipalState)
e1Base := sanityDecomposeEquationValues(e1Values[0].equation, valPrincipalState)
e2Base := sanityDecomposeEquationValues(e2Values[0].equation, valPrincipalState)
if sanityEquivalentValues(e1Base[1], e2Values[1], valPrincipalState) &&
sanityEquivalentValues(e1Values[1], e2Base[1], valPrincipalState) {
return true
......@@ -352,7 +353,7 @@ func sanityEquivalentEquations(e1 equation, e2 equation, valPrincipalState *prin
return false
}
func sanityDeconstructEquationValues(e equation, valPrincipalState *principalState) []value {
func sanityDecomposeEquationValues(e equation, valPrincipalState *principalState) []value {
var values []value
for _, v := range e.values {
switch v.kind {
......@@ -381,7 +382,8 @@ func sanityFindConstantInPrimitive(c constant, p primitive, valPrincipalState *p
case "primitive":
switch a.kind {
case "primitive":
if sanityEquivalentPrimitives(a.primitive, aa.primitive, valPrincipalState) {
equivPrim, _, _ := sanityEquivalentPrimitives(a.primitive, aa.primitive, valPrincipalState, true)
if equivPrim {
return true
}
}
......@@ -395,7 +397,7 @@ func sanityFindConstantInPrimitive(c constant, p primitive, valPrincipalState *p
return true
}
}
v := sanityDeconstructEquationValues(aa.equation, valPrincipalState)
v := sanityDecomposeEquationValues(aa.equation, valPrincipalState)
for _, vv := range v {
switch vv.kind {
case "constant":
......@@ -448,7 +450,7 @@ func sanityEquivalentValueInValues(v value, assigneds *[]value, valPrincipalStat
return index
}
func sanityPerformPrimitiveRewrite(p primitive, i int, valPrincipalState *principalState) ([]primitive, bool, value) {
func sanityPerformPrimitiveRewrite(p primitive, pi int, valPrincipalState *principalState) ([]primitive, bool, value) {
wasRewritten := false
failedRewrites := []primitive{}
rewrite := value{
......@@ -465,11 +467,6 @@ func sanityPerformPrimitiveRewrite(p primitive, i int, valPrincipalState *princi
case "constant":
rewrite.primitive.arguments = append(rewrite.primitive.arguments, p.arguments[i])
case "primitive":
prim := primitiveGet(a.primitive.name)
if !prim.rewrite.hasRule {
rewrite.primitive.arguments = append(rewrite.primitive.arguments, p.arguments[i])
continue
}
pFailedRewrite, pWasRewritten, pRewrite := sanityPerformPrimitiveRewrite(a.primitive, -1, valPrincipalState)
if pWasRewritten {
wasRewritten = true
......@@ -489,21 +486,33 @@ func sanityPerformPrimitiveRewrite(p primitive, i int, valPrincipalState *princi
}