Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Open sidebar
Verifpal
Verifpal
Commits
35e0a28a
Commit
35e0a28a
authored
Jan 05, 2021
by
Nadim Kobeissi
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Cleanup
parent
d93536ce
Pipeline
#811
passed with stages
in 1 minute and 20 seconds
Changes
8
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
41 additions
and
41 deletions
+41
-41
cmd/vplogic/inject.go
cmd/vplogic/inject.go
+1
-1
cmd/vplogic/mutationmap.go
cmd/vplogic/mutationmap.go
+0
-5
cmd/vplogic/possible.go
cmd/vplogic/possible.go
+2
-2
cmd/vplogic/sanity.go
cmd/vplogic/sanity.go
+4
-4
cmd/vplogic/types.go
cmd/vplogic/types.go
+0
-1
cmd/vplogic/value.go
cmd/vplogic/value.go
+16
-3
cmd/vplogic/verifyactive.go
cmd/vplogic/verifyactive.go
+17
-24
examples/test/concat1.vp
examples/test/concat1.vp
+1
-1
No files found.
cmd/vplogic/inject.go
View file @
35e0a28a
...
...
@@ -49,7 +49,7 @@ func injectConstantRules(c *Constant, arg int, p *Primitive) bool {
switch
{
case
p
.
Arguments
[
arg
]
.
Kind
!=
typesEnumConstant
:
return
false
case
c
.
ID
==
valueG
.
Data
.
(
*
Constant
)
.
ID
:
case
valueEquivalentConstants
(
c
,
valueG
.
Data
.
(
*
Constant
)
)
:
return
false
}
return
true
...
...
cmd/vplogic/mutationmap.go
View file @
35e0a28a
...
...
@@ -19,7 +19,6 @@ func mutationMapInit(
Mutations
:
[][]
*
Value
{},
Combination
:
[]
*
Value
{},
DepthIndex
:
[]
int
{},
Worthwhile
:
false
,
OutOfMutations
:
false
,
}
InfoMessage
(
fmt
.
Sprintf
(
...
...
@@ -206,15 +205,11 @@ func mutationMapReplaceEquation(
}
func
mutationMapNext
(
valMutationMap
MutationMap
)
MutationMap
{
valMutationMap
.
Worthwhile
=
false
if
len
(
valMutationMap
.
Combination
)
==
0
{
valMutationMap
.
OutOfMutations
=
true
return
valMutationMap
}
for
i
:=
0
;
i
<
len
(
valMutationMap
.
Combination
);
i
++
{
if
i
>=
valMutationMap
.
LastIncrement
{
valMutationMap
.
Worthwhile
=
true
}
valMutationMap
.
Combination
[
i
]
=
valMutationMap
.
Mutations
[
i
][
valMutationMap
.
DepthIndex
[
i
]]
if
i
!=
len
(
valMutationMap
.
Combination
)
-
1
{
continue
...
...
cmd/vplogic/possible.go
View file @
35e0a28a
...
...
@@ -15,8 +15,8 @@ func possibleToDecomposePrimitive(
if
!
prim
.
Decompose
.
HasRule
{
return
false
,
&
Value
{},
has
}
for
i
,
g
:=
range
prim
.
Decompose
.
Given
{
a
:=
p
.
Arguments
[
g
]
for
i
:=
0
;
i
<
len
(
prim
.
Decompose
.
Given
);
i
++
{
a
:=
p
.
Arguments
[
prim
.
Decompose
.
Given
[
i
]
]
a
,
valid
:=
prim
.
Decompose
.
Filter
(
p
,
a
,
i
)
if
!
valid
{
continue
...
...
cmd/vplogic/sanity.go
View file @
35e0a28a
...
...
@@ -60,7 +60,7 @@ func sanityAssignmentConstants(
case
typesEnumConstant
:
unique
:=
true
for
_
,
c
:=
range
constants
{
if
right
.
Data
.
(
*
Constant
)
.
ID
==
c
.
ID
{
if
valueEquivalentConstants
(
right
.
Data
.
(
*
Constant
)
,
c
)
{
unique
=
false
break
}
...
...
@@ -106,7 +106,7 @@ func sanityAssignmentConstantsFromPrimitive(
case
typesEnumConstant
:
unique
:=
true
for
_
,
c
:=
range
constants
{
if
a
.
Data
.
(
*
Constant
)
.
ID
==
c
.
ID
{
if
valueEquivalentConstants
(
a
.
Data
.
(
*
Constant
)
,
c
)
{
unique
=
false
break
}
...
...
@@ -133,7 +133,7 @@ func sanityAssignmentConstantsFromEquation(right *Value, constants []*Constant)
for
_
,
v
:=
range
right
.
Data
.
(
*
Equation
)
.
Values
{
unique
:=
true
for
_
,
c
:=
range
constants
{
if
v
.
Data
.
(
*
Constant
)
.
ID
==
c
.
ID
{
if
valueEquivalentConstants
(
v
.
Data
.
(
*
Constant
)
,
c
)
{
unique
=
false
break
}
...
...
@@ -431,7 +431,7 @@ func sanityCheckEquationRootGenerator(e *Equation) error {
}
}
if
i
>
0
{
if
c
.
Data
.
(
*
Constant
)
.
ID
==
valueG
.
Data
.
(
*
Constant
)
.
ID
{
if
valueEquivalentConstants
(
c
.
Data
.
(
*
Constant
)
,
valueG
.
Data
.
(
*
Constant
)
)
{
return
fmt
.
Errorf
(
"equation (%s) uses 'g' not as a generator"
,
prettyEquation
(
e
),
...
...
cmd/vplogic/types.go
View file @
35e0a28a
...
...
@@ -325,7 +325,6 @@ type MutationMap struct {
Constants
[]
*
Constant
Mutations
[][]
*
Value
Combination
[]
*
Value
Worthwhile
bool
DepthIndex
[]
int
}
...
...
cmd/vplogic/value.go
View file @
35e0a28a
...
...
@@ -75,7 +75,7 @@ func valueIsGOrNil(c *Constant) bool {
func
valueGetKnowledgeMapIndexFromConstant
(
valKnowledgeMap
*
KnowledgeMap
,
c
*
Constant
)
int
{
for
i
:=
range
valKnowledgeMap
.
Constants
{
if
valKnowledgeMap
.
Constants
[
i
]
.
ID
==
c
.
ID
{
if
valueEquivalentConstants
(
valKnowledgeMap
.
Constants
[
i
]
,
c
)
{
return
i
}
}
...
...
@@ -84,7 +84,7 @@ func valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap *KnowledgeMap, c *Con
func
valueGetPrincipalStateIndexFromConstant
(
valPrincipalState
*
PrincipalState
,
c
*
Constant
)
int
{
for
i
:=
range
valPrincipalState
.
Constants
{
if
valPrincipalState
.
Constants
[
i
]
.
ID
==
c
.
ID
{
if
valueEquivalentConstants
(
valPrincipalState
.
Constants
[
i
]
,
c
)
{
return
i
}
}
...
...
@@ -140,7 +140,7 @@ func valueEquivalentValues(a1 *Value, a2 *Value, considerOutput bool) bool {
}
switch
a1
.
Kind
{
case
typesEnumConstant
:
return
a1
.
Data
.
(
*
Constant
)
.
ID
==
a2
.
Data
.
(
*
Constant
)
.
ID
return
valueEquivalentConstants
(
a1
.
Data
.
(
*
Constant
)
,
a2
.
Data
.
(
*
Constant
)
)
case
typesEnumPrimitive
:
equivPrim
,
_
,
_
:=
valueEquivalentPrimitives
(
a1
.
Data
.
(
*
Primitive
),
a2
.
Data
.
(
*
Primitive
),
considerOutput
,
...
...
@@ -154,6 +154,10 @@ func valueEquivalentValues(a1 *Value, a2 *Value, considerOutput bool) bool {
return
false
}
func
valueEquivalentConstants
(
c1
*
Constant
,
c2
*
Constant
)
bool
{
return
c1
.
ID
==
c2
.
ID
}
func
valueEquivalentPrimitives
(
p1
*
Primitive
,
p2
*
Primitive
,
considerOutput
bool
,
)
(
bool
,
int
,
int
)
{
...
...
@@ -217,6 +221,15 @@ func valueEquivalentValueInValues(v *Value, a []*Value) int {
return
-
1
}
func
valueEquivalentConstantInConstants
(
c
*
Constant
,
a
[]
*
Constant
)
int
{
for
i
:=
0
;
i
<
len
(
a
);
i
++
{
if
valueEquivalentConstants
(
c
,
a
[
i
])
{
return
i
}
}
return
-
1
}
func
valuePerformPrimitiveRewrite
(
p
*
Primitive
,
pi
int
,
valPrincipalState
*
PrincipalState
,
)
([]
*
Primitive
,
bool
,
*
Value
)
{
...
...
cmd/vplogic/verifyactive.go
View file @
35e0a28a
...
...
@@ -90,10 +90,10 @@ func verifyActiveScan(
scanGroup
.
Done
()
return
err
}
if
valMutationMap
.
Worthwhile
{
valPrincipalStateMutated
:=
verifyActiveMutatePrincipalState
(
constructPrincipalStateClone
(
valPrincipalState
,
true
),
valAttackerState
,
valMutationMap
,
)
valPrincipalStateMutated
,
isWorthwhileMutation
:=
verifyActiveMutatePrincipalState
(
constructPrincipalStateClone
(
valPrincipalState
,
true
),
valAttackerState
,
valMutationMap
,
)
if
isWorthwhileMutation
{
scanGroup
.
Add
(
1
)
go
func
()
{
err
=
verifyAnalysis
(
...
...
@@ -123,7 +123,8 @@ func verifyActiveScan(
func
verifyActiveMutatePrincipalState
(
valPrincipalState
*
PrincipalState
,
valAttackerState
AttackerState
,
valMutationMap
MutationMap
,
)
*
PrincipalState
{
)
(
*
PrincipalState
,
bool
)
{
isWorthwhileMutation
:=
false
MutationLoop
:
for
i
:=
0
;
i
<
len
(
valMutationMap
.
Constants
);
i
++
{
ai
,
ii
:=
valueResolveConstant
(
valMutationMap
.
Constants
[
i
],
valPrincipalState
)
...
...
@@ -131,31 +132,17 @@ MutationLoop:
ar
,
_
:=
valueResolveValueInternalValuesFromPrincipalState
(
ai
,
ai
,
ii
,
valPrincipalState
,
valAttackerState
,
true
,
)
switch
ar
.
Kind
{
case
typesEnumPrimitive
:
_
,
aar
:=
possibleToRewrite
(
ar
.
Data
.
(
*
Primitive
),
valPrincipalState
)
switch
aar
[
0
]
.
Kind
{
case
typesEnumPrimitive
:
ar
.
Data
=
aar
[
0
]
.
Data
.
(
*
Primitive
)
}
}
switch
ac
.
Kind
{
case
typesEnumPrimitive
:
_
,
aac
:=
possibleToRewrite
(
ac
.
Data
.
(
*
Primitive
),
valPrincipalState
)
switch
aac
[
0
]
.
Kind
{
case
typesEnumPrimitive
:
ac
.
Data
=
aac
[
0
]
.
Data
.
(
*
Primitive
)
}
switch
ar
.
Kind
{
case
typesEnumPrimitive
:
ac
.
Data
.
(
*
Primitive
)
.
Output
=
ar
.
Data
.
(
*
Primitive
)
.
Output
ac
.
Data
.
(
*
Primitive
)
.
Check
=
ar
.
Data
.
(
*
Primitive
)
.
Check
}
acc
:=
valueGetConstantsFromValue
(
ac
)
for
acci
:=
0
;
acci
<
len
(
acc
);
acci
++
{
if
acc
[
acci
]
.
ID
==
valMutationMap
.
Constants
[
i
]
.
ID
{
continue
MutationLoop
}
if
valueEquivalentConstantInConstants
(
valMutationMap
.
Constants
[
i
],
valueGetConstantsFromValue
(
ac
),
)
>=
0
{
continue
MutationLoop
}
}
switch
{
...
...
@@ -167,6 +154,12 @@ MutationLoop:
valPrincipalState
.
Mutated
[
ii
]
=
true
valPrincipalState
.
Assigned
[
ii
]
=
ac
valPrincipalState
.
BeforeRewrite
[
ii
]
=
ac
if
i
>=
valMutationMap
.
LastIncrement
{
isWorthwhileMutation
=
true
}
}
if
!
isWorthwhileMutation
{
return
valPrincipalState
,
isWorthwhileMutation
}
valPrincipalState
,
_
=
valueResolveAllPrincipalStateValues
(
valPrincipalState
,
valAttackerState
)
failedRewrites
,
failedRewriteIndices
,
valPrincipalState
:=
valuePerformAllRewrites
(
valPrincipalState
)
...
...
@@ -194,7 +187,7 @@ FailedRewritesLoop:
}
}
}
return
valPrincipalState
return
valPrincipalState
,
isWorthwhileMutation
}
func
verifyActiveDropPrincipalStateAfterIndex
(
valPrincipalState
*
PrincipalState
,
f
int
)
*
PrincipalState
{
...
...
examples/test/concat1.vp
View file @
35e0a28a
...
...
@@ -20,4 +20,4 @@ principal Bob[
queries[
confidentiality? m
]
\ No newline at end of file
]
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment