verifyactive.go 7.35 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
// 7d5d2341a999bccff8fc2ff129fefc89

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

Nadim Kobeissi's avatar
Nadim Kobeissi committed
7
import (
Nadim Kobeissi's avatar
Nadim Kobeissi committed
8
	"fmt"
Nadim Kobeissi's avatar
Nadim Kobeissi committed
9
10
	"sync"
)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
11

12
func verifyActive(valKnowledgeMap *KnowledgeMap, valPrincipalStates []*PrincipalState) error {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
13
	InfoMessage("Attacker is configured as active.", "info", false)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
14
	phase := 0
Nadim Kobeissi's avatar
Nadim Kobeissi committed
15
	for phase <= valKnowledgeMap.MaxPhase {
16
		var stageGroup sync.WaitGroup
Nadim Kobeissi's avatar
Nadim Kobeissi committed
17
		InfoMessage(fmt.Sprintf("Running at phase %d.", phase), "info", false)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
18
		attackerStateInit(true)
19
		valPrincipalStatePureResolved := constructPrincipalStateClone(valPrincipalStates[0], true)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
20
21
22
		valPrincipalStatePureResolved, err := valueResolveAllPrincipalStateValues(
			valPrincipalStatePureResolved, attackerStateGetRead(),
		)
23
24
25
26
		if err != nil {
			return err
		}
		err = attackerStatePutPhaseUpdate(valPrincipalStatePureResolved, phase)
27
28
29
30
31
32
33
		if err != nil {
			return err
		}
		err = verifyStandardRun(valKnowledgeMap, valPrincipalStates, 0)
		if err != nil {
			return err
		}
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
		stageGroup.Add(1)
		go verifyActiveStages(1, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
		stageGroup.Wait()
		stageGroup.Add(2)
		go verifyActiveStages(2, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
		go verifyActiveStages(3, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
		stageGroup.Wait()
		stageGroup.Add(2)
		go verifyActiveStages(4, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
		go verifyActiveStages(5, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
		stageGroup.Wait()
		stage := 6
		for !verifyResultsAllResolved() && !attackerStateGetExhausted() {
			stageGroup.Add(1)
			go verifyActiveStages(stage, valKnowledgeMap, valPrincipalStates, attackerStateGetRead(), &stageGroup)
			stageGroup.Wait()
			stage = stage + 1
Nadim Kobeissi's avatar
Nadim Kobeissi committed
51
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
52
		phase = phase + 1
Nadim Kobeissi's avatar
Nadim Kobeissi committed
53
	}
54
	return nil
Nadim Kobeissi's avatar
Nadim Kobeissi committed
55
56
}

57
func verifyActiveStages(
58
	stage int, valKnowledgeMap *KnowledgeMap, valPrincipalStates []*PrincipalState,
59
	valAttackerState AttackerState, stageGroup *sync.WaitGroup,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
60
) {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
61
	var principalGroup sync.WaitGroup
Nadim Kobeissi's avatar
Nadim Kobeissi committed
62
	var err error
63
64
	oldKnown := len(valAttackerState.Known)
	valAttackerState = attackerStateGetRead()
Nadim Kobeissi's avatar
Nadim Kobeissi committed
65
	principalGroup.Add(len(valPrincipalStates))
66
	for _, valPrincipalState := range valPrincipalStates {
67
		go func(valPrincipalState *PrincipalState) {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
68
			var scanGroup sync.WaitGroup
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
			var valMutationMap MutationMap
			valMutationMap, err = mutationMapInit(
				valKnowledgeMap, valPrincipalState, valAttackerState, stage,
			)
			if err != nil {
				scanGroup.Done()
				return
			}
			scanGroup.Add(1)
			err = verifyActiveScan(
				valKnowledgeMap, valPrincipalState, valAttackerState,
				mutationMapNext(valMutationMap), stage, &scanGroup,
			)
			if err != nil {
				scanGroup.Done()
				return
			}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
86
87
			scanGroup.Wait()
			principalGroup.Done()
88
		}(valPrincipalState)
89
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
90
	principalGroup.Wait()
91
92
93
94
95
	exhausted := (stage > 5 && (oldKnown == len(valAttackerState.Known)))
	if exhausted {
		attackerStatePutExhausted()
	}
	stageGroup.Done()
96
97
}

Nadim Kobeissi's avatar
Nadim Kobeissi committed
98
func verifyActiveScan(
99
	valKnowledgeMap *KnowledgeMap, valPrincipalState *PrincipalState,
100
101
	valAttackerState AttackerState, valMutationMap MutationMap,
	stage int, scanGroup *sync.WaitGroup,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
102
103
) error {
	var err error
Nadim Kobeissi's avatar
Nadim Kobeissi committed
104
	if verifyResultsAllResolved() {
105
		scanGroup.Done()
106
		return err
Nadim Kobeissi's avatar
Nadim Kobeissi committed
107
	}
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
108
109
110
111
	valPrincipalStateMutated, isWorthwhileMutation := verifyActiveMutatePrincipalState(
		constructPrincipalStateClone(valPrincipalState, true), valAttackerState, valMutationMap,
	)
	if isWorthwhileMutation {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
112
		scanGroup.Add(1)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
113
114
		go func() {
			err = verifyAnalysis(
Nadim Kobeissi's avatar
Nadim Kobeissi committed
115
				valKnowledgeMap, valPrincipalStateMutated, attackerStateGetRead(), stage, scanGroup,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
116
117
118
119
120
121
			)
			if err != nil {
				scanGroup.Done()
				return
			}
		}()
Nadim Kobeissi's avatar
Nadim Kobeissi committed
122
	}
123
124
	if valMutationMap.OutOfMutations {
		scanGroup.Done()
125
		return err
Nadim Kobeissi's avatar
Nadim Kobeissi committed
126
	}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
127
128
129
130
131
132
133
134
135
136
	go func() {
		err := verifyActiveScan(
			valKnowledgeMap, valPrincipalState, valAttackerState,
			mutationMapNext(valMutationMap), stage, scanGroup,
		)
		if err != nil {
			scanGroup.Done()
		}
	}()
	return nil
Nadim Kobeissi's avatar
Nadim Kobeissi committed
137
138
}

Nadim Kobeissi's avatar
Nadim Kobeissi committed
139
func verifyActiveMutatePrincipalState(
140
	valPrincipalState *PrincipalState, valAttackerState AttackerState, valMutationMap MutationMap,
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
141
) (*PrincipalState, bool) {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
142
	earliestMutation := len(valPrincipalState.Constants)
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
143
	isWorthwhileMutation := false
144
MutationLoop:
145
146
	for i := 0; i < len(valMutationMap.Constants); i++ {
		ai, ii := valueResolveConstant(valMutationMap.Constants[i], valPrincipalState)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
147
		ac := valMutationMap.Combination[i]
148
		ar, _ := valueResolveValueInternalValuesFromPrincipalState(
Nadim Kobeissi's avatar
Nadim Kobeissi committed
149
			ai, ai, ii, valPrincipalState, valAttackerState, true,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
150
		)
151
		switch ac.Kind {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
152
		case typesEnumPrimitive:
153
154
			switch ar.Kind {
			case typesEnumPrimitive:
155
156
				ac.Data.(*Primitive).Output = ar.Data.(*Primitive).Output
				ac.Data.(*Primitive).Check = ar.Data.(*Primitive).Check
157
			}
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
158
159
160
161
			if valueEquivalentConstantInConstants(
				valMutationMap.Constants[i], valueGetConstantsFromValue(ac),
			) >= 0 {
				continue MutationLoop
162
			}
163
		}
164
165
166
		switch {
		case valueEquivalentValues(ac, ar, true):
			continue
Nadim Kobeissi's avatar
WIP.    
Nadim Kobeissi committed
167
		}
168
169
		valPrincipalState.Creator[ii] = principalNamesMap["Attacker"]
		valPrincipalState.Sender[ii] = principalNamesMap["Attacker"]
Nadim Kobeissi's avatar
Nadim Kobeissi committed
170
171
172
		valPrincipalState.Mutated[ii] = true
		valPrincipalState.Assigned[ii] = ac
		valPrincipalState.BeforeRewrite[ii] = ac
Nadim Kobeissi's avatar
Nadim Kobeissi committed
173
174
175
		if ii < earliestMutation {
			earliestMutation = ii
		}
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
176
177
178
179
180
181
		if i >= valMutationMap.LastIncrement {
			isWorthwhileMutation = true
		}
	}
	if !isWorthwhileMutation {
		return valPrincipalState, isWorthwhileMutation
182
	}
183
	valPrincipalState, _ = valueResolveAllPrincipalStateValues(valPrincipalState, valAttackerState)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
184
	failedRewrites, failedRewriteIndices, valPrincipalState := valuePerformAllRewrites(valPrincipalState)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
185
186
	for i := 0; i < len(failedRewrites); i++ {
		if !failedRewrites[i].Check {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
187
188
			continue
		}
189
		if valPrincipalState.Creator[failedRewriteIndices[i]] != valPrincipalState.ID {
190
191
			continue
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
192
		declaredAt := valPrincipalState.DeclaredAt[failedRewriteIndices[i]]
Nadim Kobeissi's avatar
Nadim Kobeissi committed
193
		if declaredAt == valPrincipalState.MaxDeclaredAt {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
194
195
196
			valPrincipalState = verifyActiveDropPrincipalStateAfterIndex(
				valPrincipalState, failedRewriteIndices[i]+1,
			)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
197
			return valPrincipalState, isWorthwhileMutation && earliestMutation < failedRewriteIndices[i]
Nadim Kobeissi's avatar
Nadim Kobeissi committed
198
		}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
199
200
		for ii := 0; ii < len(valPrincipalState.Constants); ii++ {
			if valPrincipalState.DeclaredAt[ii] == declaredAt {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
201
				valPrincipalState = verifyActiveDropPrincipalStateAfterIndex(
Nadim Kobeissi's avatar
Nadim Kobeissi committed
202
					valPrincipalState, ii+1,
Nadim Kobeissi's avatar
Nadim Kobeissi committed
203
				)
Nadim Kobeissi's avatar
Nadim Kobeissi committed
204
				return valPrincipalState, isWorthwhileMutation && earliestMutation < failedRewriteIndices[i]
Nadim Kobeissi's avatar
Nadim Kobeissi committed
205
			}
Nadim Kobeissi's avatar
Nadim Kobeissi committed
206
207
		}
	}
Nadim Kobeissi's avatar
Cleanup    
Nadim Kobeissi committed
208
	return valPrincipalState, isWorthwhileMutation
Nadim Kobeissi's avatar
WIP.    
Nadim Kobeissi committed
209
210
}

211
func verifyActiveDropPrincipalStateAfterIndex(valPrincipalState *PrincipalState, f int) *PrincipalState {
Nadim Kobeissi's avatar
Nadim Kobeissi committed
212
213
214
215
216
217
218
219
220
221
222
223
	valPrincipalState.Constants = valPrincipalState.Constants[:f]
	valPrincipalState.Assigned = valPrincipalState.Assigned[:f]
	valPrincipalState.Guard = valPrincipalState.Guard[:f]
	valPrincipalState.Known = valPrincipalState.Known[:f]
	valPrincipalState.KnownBy = valPrincipalState.KnownBy[:f]
	valPrincipalState.Creator = valPrincipalState.Creator[:f]
	valPrincipalState.Sender = valPrincipalState.Sender[:f]
	valPrincipalState.Rewritten = valPrincipalState.Rewritten[:f]
	valPrincipalState.BeforeRewrite = valPrincipalState.BeforeRewrite[:f]
	valPrincipalState.Mutated = valPrincipalState.Mutated[:f]
	valPrincipalState.BeforeMutate = valPrincipalState.BeforeMutate[:f]
	valPrincipalState.Phase = valPrincipalState.Phase[:f]
Nadim Kobeissi's avatar
Nadim Kobeissi committed
224
	return valPrincipalState
Nadim Kobeissi's avatar
Nadim Kobeissi committed
225
}