verify.go 5.31 KB
Newer Older
Nadim Kobeissi's avatar
Nadim Kobeissi committed
1
/* SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
Nadim Kobeissi's avatar
Nadim Kobeissi committed
2
 * SPDX-License-Identifier: GPL-3.0-only */
Nadim Kobeissi's avatar
Nadim Kobeissi committed
3
4
// 458871bd68906e9965785ac87c2708ec

5
package vplogic
Nadim Kobeissi's avatar
Nadim Kobeissi committed
6
7
8

import (
	"fmt"
9
	"os"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
10
	"sync"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
11
12
13
	"time"
)

Nadim Kobeissi's avatar
Nadim Kobeissi committed
14
// Verify runs the main verification engine for Verifpal on a model loaded from a file.
Nadim Kobeissi's avatar
Comment    
Nadim Kobeissi committed
15
// It returns a slice of verifyResults and a "results code".
16
func Verify(filePath string) ([]VerifyResult, string, error) {
17
18
19
20
21
	/*
		f, _ := os.Create("cpu.pprof")
		pprof.StartCPUProfile(f)
		defer pprof.StopCPUProfile()
	*/
22
23
24
25
	m, err := libpegParseModel(filePath, true)
	if err != nil {
		return []VerifyResult{}, "", err
	}
26
27
28
	return verifyModel(m)
}

29
30
31
32
33
func verifyModel(m Model) ([]VerifyResult, string, error) {
	valKnowledgeMap, valPrincipalStates, err := sanity(m)
	if err != nil {
		return []VerifyResult{}, "", err
	}
34
	initiated := time.Now().Format("03:04:05 PM")
Nadim Kobeissi's avatar
Nadim Kobeissi committed
35
	verifyAnalysisCountInit()
Nadim Kobeissi's avatar
Nadim Kobeissi committed
36
	verifyResultsInit(m)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
37
	InfoMessage(fmt.Sprintf(
Nadim Kobeissi's avatar
Nadim Kobeissi committed
38
		"Verification initiated for '%s' at %s.", m.FileName, initiated,
39
	), "verifpal", false)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
40
	switch m.Attacker {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
41
	case "passive":
42
43
44
45
		err := verifyPassive(valKnowledgeMap, valPrincipalStates)
		if err != nil {
			return []VerifyResult{}, "", err
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
46
	case "active":
47
48
49
50
		err := verifyActive(valKnowledgeMap, valPrincipalStates)
		if err != nil {
			return []VerifyResult{}, "", err
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
51
	default:
52
		return []VerifyResult{}, "", fmt.Errorf("invalid attacker (%s)", m.Attacker)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
53
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
54
	return verifyEnd(m)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
55
56
}

Nadim Kobeissi's avatar
Nadim Kobeissi committed
57
func verifyResolveQueries(
58
	valKnowledgeMap *KnowledgeMap, valPrincipalState *PrincipalState,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
59
) error {
60
	valVerifyResults, _ := verifyResultsGetRead()
61
	for _, verifyResult := range valVerifyResults {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
62
		if !verifyResult.Resolved {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
63
64
65
66
			err := queryStart(verifyResult.Query, valKnowledgeMap, valPrincipalState)
			if err != nil {
				return err
			}
Nadim Kobeissi's avatar
WIP.    
Nadim Kobeissi committed
67
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
68
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
69
	return nil
Nadim Kobeissi's avatar
Nadim Kobeissi committed
70
}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
71

72
func verifyStandardRun(valKnowledgeMap *KnowledgeMap, valPrincipalStates []*PrincipalState, stage int) error {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
73
	var scanGroup sync.WaitGroup
74
	valAttackerState := attackerStateGetRead()
75
76
	for _, valPrincipalState := range valPrincipalStates {
		var err error
Nadim Kobeissi's avatar
Nadim Kobeissi committed
77
78
		var failedRewrites []*Primitive
		valPrincipalState, err = valueResolveAllPrincipalStateValues(valPrincipalState, valAttackerState)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
79
80
81
82
83
		if err != nil {
			return err
		}
		for _, a := range valPrincipalState.Assigned {
			switch a.Kind {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
84
			case typesEnumPrimitive:
85
				injectMissingSkeletons(a.Data.(*Primitive), valPrincipalState, valAttackerState)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
86
87
			}
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
88
		failedRewrites, _, valPrincipalState = valuePerformAllRewrites(valPrincipalState)
89
90
91
92
		err = sanityFailOnFailedCheckedPrimitiveRewrite(failedRewrites)
		if err != nil {
			return err
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
93
		for i := range valPrincipalState.Assigned {
94
			err = sanityCheckEquationGenerators(valPrincipalState.Assigned[i])
95
96
97
			if err != nil {
				return err
			}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
98
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
99
		scanGroup.Add(1)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
100
101
102
103
		err = verifyAnalysis(valKnowledgeMap, valPrincipalState, valAttackerState, stage, &scanGroup)
		if err != nil {
			return err
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
104
		scanGroup.Wait()
Nadim Kobeissi's avatar
Nadim Kobeissi committed
105
106
107
108
		err = verifyResolveQueries(valKnowledgeMap, valPrincipalState)
		if err != nil {
			return err
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
109
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
110
	return nil
Nadim Kobeissi's avatar
Nadim Kobeissi committed
111
112
}

113
func verifyPassive(valKnowledgeMap *KnowledgeMap, valPrincipalStates []*PrincipalState) error {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
114
	InfoMessage("Attacker is configured as passive.", "info", false)
115
	phase := 0
Nadim Kobeissi's avatar
Nadim Kobeissi committed
116
	for phase <= valKnowledgeMap.MaxPhase {
117
		attackerStateInit(false)
118
		valPrincipalStatePureResolved := constructPrincipalStateClone(valPrincipalStates[0], true)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
119
120
121
		valPrincipalStatePureResolved, err := valueResolveAllPrincipalStateValues(
			valPrincipalStatePureResolved, attackerStateGetRead(),
		)
122
123
124
125
		if err != nil {
			return err
		}
		err = attackerStatePutPhaseUpdate(valPrincipalStatePureResolved, phase)
126
127
128
129
130
131
132
		if err != nil {
			return err
		}
		err = verifyStandardRun(valKnowledgeMap, valPrincipalStates, 0)
		if err != nil {
			return err
		}
133
134
		phase = phase + 1
	}
135
	return nil
Nadim Kobeissi's avatar
Nadim Kobeissi committed
136
137
}

Nadim Kobeissi's avatar
Nadim Kobeissi committed
138
func verifyGetResultsCode(valVerifyResults []VerifyResult) string {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
139
140
	resultsCode := ""
	for _, verifyResult := range valVerifyResults {
141
142
		q := ""
		r := ""
Nadim Kobeissi's avatar
Nadim Kobeissi committed
143
		switch verifyResult.Query.Kind {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
144
		case typesEnumConfidentiality:
145
			q = "c"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
146
		case typesEnumAuthentication:
Nadim Kobeissi's avatar
Nadim Kobeissi committed
147
			q = "a"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
148
		case typesEnumFreshness:
149
			q = "f"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
150
		case typesEnumUnlinkability:
151
			q = "u"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
152
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
153
		switch verifyResult.Resolved {
154
		case true:
Nadim Kobeissi's avatar
Nadim Kobeissi committed
155
			r = "1"
156
157
		case false:
			r = "0"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
158
159
160
161
162
163
164
165
166
		}
		resultsCode = fmt.Sprintf(
			"%s%s%s",
			resultsCode, q, r,
		)
	}
	return resultsCode
}

167
168
func verifyEnd(m Model) ([]VerifyResult, string, error) {
	var err error
169
	valVerifyResults, fileName := verifyResultsGetRead()
170
171
172
173
174
175
176
	noResolved := true
	for _, verifyResult := range valVerifyResults {
		if verifyResult.Resolved {
			noResolved = false
			break
		}
	}
177
178
	fmt.Fprint(os.Stdout, "\n\n")
	InfoMessage(fmt.Sprintf(
179
180
		"Verification completed for '%s' at %s.",
		fileName, time.Now().Format("03:04:05 PM"),
181
	), "verifpal", false)
182
183
184
185
186
	if noResolved {
		InfoMessage("All queries pass.", "verifpal", false)
	} else {
		InfoMessage("Summary of failed queries will follow.", "verifpal", false)
	}
187
	fmt.Fprint(os.Stdout, "\n")
188
	for _, verifyResult := range valVerifyResults {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
189
		if verifyResult.Resolved {
190
191
			InfoMessage(fmt.Sprintf("%s — %s",
				prettyQuery(verifyResult.Query), verifyResult.Summary,
192
			), "result", false)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
193
194
		}
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
195
	InfoMessage("Thank you for using Verifpal.", "verifpal", false)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
196
197
	resultsCode := verifyGetResultsCode(valVerifyResults)
	if VerifHubScheduledShared {
198
		err = VerifHub(m, fileName, resultsCode)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
199
	}
200
	return valVerifyResults, resultsCode, err
Nadim Kobeissi's avatar
Nadim Kobeissi committed
201
}