1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
|
from functools import total_ordering
from typing import Self
from snapshot import ProgramState, MemoryAccessError
from symbolic import SymbolicTransform
@total_ordering
class ErrorSeverity:
def __init__(self, num: int, name: str):
"""Construct an error severity.
:param num: A numerical value that orders the severity with respect
to other `ErrorSeverity` objects. Smaller values are less
severe.
:param name: A descriptive name for the error severity, e.g. 'fatal'
or 'info'.
"""
self._numeral = num
self.name = name
def __repr__(self) -> str:
return f'[{self.name}]'
def __eq__(self, other: Self) -> bool:
return self._numeral == other._numeral
def __lt__(self, other: Self) -> bool:
return self._numeral < other._numeral
def __hash__(self) -> int:
return hash(self._numeral)
class ErrorTypes:
INFO = ErrorSeverity(0, 'INFO')
INCOMPLETE = ErrorSeverity(2, 'INCOMPLETE DATA')
POSSIBLE = ErrorSeverity(4, 'UNCONFIRMED ERROR')
CONFIRMED = ErrorSeverity(5, 'ERROR')
class Error:
"""A state comparison error."""
def __init__(self, severity: ErrorSeverity, msg: str):
self.severity = severity
self.error_msg = msg
def __repr__(self) -> str:
return f'{self.severity} {self.error_msg}'
def _calc_transformation(previous: ProgramState, current: ProgramState):
"""Calculate the difference between two context blocks.
:return: A context block that contains in its registers the difference
between the corresponding input blocks' register values.
"""
assert(previous.arch == current.arch)
arch = previous.arch
transformation = ProgramState(arch)
for reg in arch.regnames:
try:
prev_val, cur_val = previous.read(reg), current.read(reg)
if prev_val is not None and cur_val is not None:
transformation.set(reg, cur_val - prev_val)
except ValueError:
# Register is not set in either state
pass
return transformation
def _find_errors(transform_txl: ProgramState, transform_truth: ProgramState) \
-> list[Error]:
"""Find possible errors between a reference and a tested state.
:param txl_state: The translated state to check for errors.
:param prev_txl_state: The translated snapshot immediately preceding
`txl_state`.
:param truth_state: The reference state against which to check the
translated state `txl_state` for errors.
:param prev_truth_state: The reference snapshot immediately preceding
`prev_truth_state`.
:return: A list of errors; one entry for each register that may have
faulty contents. Is empty if no errors were found.
"""
assert(transform_truth.arch == transform_txl.arch)
errors = []
for reg in transform_truth.arch.regnames:
try:
diff_txl = transform_txl.read(reg)
diff_truth = transform_truth.read(reg)
except ValueError:
errors.append(Error(ErrorTypes.INFO,
f'Value for register {reg} is not set in'
f' either the tested or the reference state.'))
continue
if diff_txl != diff_truth:
errors.append(Error(
ErrorTypes.CONFIRMED,
f'Transformation of register {reg} is false.'
f' Expected difference: {hex(diff_truth)},'
f' actual difference in the translation: {hex(diff_txl)}.'))
return errors
def compare_simple(test_states: list[ProgramState],
truth_states: list[ProgramState]) -> list[dict]:
"""Simple comparison of programs.
:param test_states: A program flow to check for errors.
:param truth_states: A reference program flow that defines a correct
program execution.
:return: Information, including possible errors, about each processed
snapshot.
"""
PC_REGNAME = 'PC'
if len(test_states) == 0:
print('No states to compare. Exiting.')
return []
# No errors in initial snapshot because we can't perform difference
# calculations on it
result = [{
'pc': test_states[0].read(PC_REGNAME),
'txl': test_states[0], 'ref': truth_states[0],
'errors': []
}]
it_prev = zip(iter(test_states), iter(truth_states))
it_cur = zip(iter(test_states[1:]), iter(truth_states[1:]))
for txl, truth in it_cur:
prev_txl, prev_truth = next(it_prev)
pc_txl = txl.read(PC_REGNAME)
pc_truth = truth.read(PC_REGNAME)
# The program counter should always be set on a snapshot
assert(pc_truth is not None)
assert(pc_txl is not None)
if pc_txl != pc_truth:
print(f'Unmatched program counter {hex(txl.read(PC_REGNAME))}'
f' in translated code!')
continue
transform_truth = _calc_transformation(prev_truth, truth)
transform_txl = _calc_transformation(prev_txl, txl)
errors = _find_errors(transform_txl, transform_truth)
result.append({
'pc': pc_txl,
'txl': transform_txl, 'ref': transform_truth,
'errors': errors
})
return result
def _find_register_errors(txl_from: ProgramState,
txl_to: ProgramState,
transform_truth: SymbolicTransform) \
-> list[Error]:
"""Find errors in register values.
Errors might be:
- A register value was modified, but the tested state contains no
reference value for that register.
- The tested destination state's value for a register does not match
the value expected by the symbolic transformation.
"""
# Calculate expected register values
try:
truth = transform_truth.calc_register_transform(txl_from)
except MemoryAccessError as err:
s, e = transform_truth.range
return [Error(
ErrorTypes.INCOMPLETE,
f'Register transformations {hex(s)} -> {hex(e)} depend on'
f' {err.mem_size} bytes at memory address {hex(err.mem_addr)}'
f' that are not entirely present in the tested state'
f' {hex(txl_from.read("pc"))}. Skipping.',
)]
# Compare expected values to actual values in the tested state
errors = []
for regname, truth_val in truth.items():
try:
txl_val = txl_to.read(regname)
except ValueError:
errors.append(Error(ErrorTypes.INCOMPLETE,
f'Value of register {regname} has changed, but'
f' is not set in the tested state. Skipping.'))
continue
except KeyError as err:
print(f'[WARNING] {err}')
continue
if txl_val != truth_val:
errors.append(Error(ErrorTypes.CONFIRMED,
f'Content of register {regname} is false.'
f' Expected value: {hex(truth_val)}, actual'
f' value in the translation: {hex(txl_val)}.'))
return errors
def _find_memory_errors(txl_from: ProgramState,
txl_to: ProgramState,
transform_truth: SymbolicTransform) \
-> list[Error]:
"""Find errors in memory values.
Errors might be:
- A range of memory was written, but the tested state contains no
reference value for that range.
- The tested destination state's content for the tested range does not
match the value expected by the symbolic transformation.
"""
# Calculate expected register values
try:
truth = transform_truth.calc_memory_transform(txl_from)
except MemoryAccessError as err:
s, e = transform_truth.range
return [Error(ErrorTypes.INCOMPLETE,
f'Memory transformations {hex(s)} -> {hex(e)} depend on'
f' {err.mem_size} bytes at memory address {hex(err.mem_addr)}'
f' that are not entirely present in the tested state'
f' {hex(txl_from.read("pc"))}. Skipping.')]
# Compare expected values to actual values in the tested state
errors = []
for addr, truth_bytes in truth.items():
size = len(truth_bytes)
try:
txl_bytes = txl_to.read_memory(addr, size)
except MemoryAccessError:
errors.append(Error(ErrorTypes.POSSIBLE,
f'Memory range [{addr}, {addr + size}) is not'
f' set in the tested result state. Skipping.'))
continue
if txl_bytes != truth_bytes:
errors.append(Error(ErrorTypes.CONFIRMED,
f'Content of memory at {addr} is false.'
f' Expected content: {truth_bytes.hex()}, actual'
f' content in the translation: {txl_bytes.hex()}.'))
return errors
def _find_errors_symbolic(txl_from: ProgramState,
txl_to: ProgramState,
transform_truth: SymbolicTransform) \
-> list[Error]:
"""Tries to find errors in transformations between tested states.
Applies a transformation to a source state and tests whether the result
matches a given destination state.
:param txl_from: Source state. This is a state from the tested
program, and is assumed as the starting point for
the transformation.
:param txl_to: Destination state. This is a possibly faulty state
from the tested program, and is tested for
correctness with respect to the source state.
:param transform_truth: The symbolic transformation that maps the source
state to the destination state.
"""
if (txl_from.read('PC') != transform_truth.range[0]) \
or (txl_to.read('PC') != transform_truth.range[1]):
tstart, tend = transform_truth.range
return [Error(ErrorTypes.POSSIBLE,
f'Program counters of the tested transformation'
f' do not match the truth transformation:'
f' {hex(txl_from.read("PC"))} -> {hex(txl_to.read("PC"))}'
f' (test) vs. {hex(tstart)} -> {hex(tend)} (truth).'
f' Skipping with no errors.')]
errors = []
errors.extend(_find_register_errors(txl_from, txl_to, transform_truth))
errors.extend(_find_memory_errors(txl_from, txl_to, transform_truth))
return errors
def compare_symbolic(test_states: list[ProgramState],
transforms: list[SymbolicTransform]) \
-> list[dict]:
#assert(len(test_states) == len(transforms) - 1)
result = [{
'pc': test_states[0].read('PC'),
'txl': test_states[0],
'ref': transforms[0],
'errors': []
}]
_list = zip(test_states[:-1], test_states[1:], transforms)
for cur_state, next_state, transform in _list:
pc_cur = cur_state.read('PC')
pc_next = next_state.read('PC')
start_addr, end_addr = transform.range
if pc_cur != start_addr:
print(f'Program counter {hex(pc_cur)} in translated code has no'
f' corresponding reference state! Skipping.'
f' (reference: {hex(start_addr)})')
continue
if pc_next != end_addr:
print(f'Tested state transformation is {hex(pc_cur)} ->'
f' {hex(pc_next)}, but reference transform is'
f' {hex(start_addr)} -> {hex(end_addr)}!'
f' Skipping.')
errors = _find_errors_symbolic(cur_state, next_state, transform)
result.append({
'pc': pc_cur,
'txl': _calc_transformation(cur_state, next_state),
'ref': transform,
'errors': errors
})
return result
|