WEBVTT

1
00:00:00.000 --> 00:00:03.822
The controller is checking an unauthorized image.

2
00:00:03.822 --> 00:00:09.802
Its six-bit state changes from CHECK to RELEASE
without a completed authorization.

3
00:00:09.802 --> 00:00:11.318
The new code is legal.

4
00:00:11.318 --> 00:00:14.771
A state decoder recognizes it and opens the gate.

5
00:00:14.771 --> 00:00:18.923
We first count which substitutions can do that.

6
00:00:19.208 --> 00:00:24.520
A finite-state machine, FSM, stores its current
phase in a register.

7
00:00:24.520 --> 00:00:30.249
Sparse encoding assigns a small set of legal
values within a larger bit space.

8
00:00:30.249 --> 00:00:36.654
The unassigned values are useful only if the
implementation recognizes them and rejects unsafe

9
00:00:36.654 --> 00:00:37.597
outputs.

10
00:00:37.875 --> 00:00:44.732
Our original six-bit map is WAIT=000000,
CHECK=001111, RELEASE=110011 and ERROR=111100.

11
00:00:44.732 --> 00:00:48.231
All six distinct state pairs differ in four bits.

12
00:00:48.231 --> 00:00:55.059
Checking only CHECK-to-RELEASE would miss a
closer pair elsewhere; the minimum must cover the

13
00:00:55.059 --> 00:00:56.262
entire map.

14
00:00:56.542 --> 00:01:03.730
One, two or three stored-bit flips cannot turn
any named state into another named state in this

15
00:01:03.730 --> 00:01:04.084
map.

16
00:01:04.084 --> 00:01:06.296
They produce invalid values.

17
00:01:06.296 --> 00:01:09.392
Four flips can reach another valid state.

18
00:01:09.392 --> 00:01:15.187
Distance therefore supports a bounded
substitution claim when the legality check and

19
00:01:15.187 --> 00:01:17.311
output gate remain trusted.

20
00:01:17.583 --> 00:01:23.959
A default branch that sends the next state to
ERROR runs after the current accepting edge.

21
00:01:23.959 --> 00:01:30.712
If an unsafe output decoder already permits an
invalid current state, next-cycle recovery is too

22
00:01:30.712 --> 00:01:31.124
late.

23
00:01:31.124 --> 00:01:39.276
Decode RELEASE with full equality and let present
invalid state suppress the same accepting edge.

24
00:01:39.542 --> 00:01:42.790
Our small decoder grants only state==RELEASE.

25
00:01:42.790 --> 00:01:45.839
Invalid states are reported separately as bad.

26
00:01:45.839 --> 00:01:51.479
A sticky flag could record them for later
recovery; it cannot replace current blocking.

27
00:01:51.479 --> 00:01:58.327
In this specific decoder equality already rejects
invalid states, so do not claim a second gate

28
00:01:58.327 --> 00:02:00.772
independently adds coverage.

29
00:02:01.042 --> 00:02:06.280
An encoding constant in RTL does not prove that
synthesis preserves it.

30
00:02:06.280 --> 00:02:11.654
Examine recoding, register width and output cones
in the produced netlist.

31
00:02:11.654 --> 00:02:17.422
OpenTitan provides a primitive flop wrapper for
sparse FSM storage; its assertions and

32
00:02:17.422 --> 00:02:22.198
instantiation do not by themselves prove a
complete controller secure.

33
00:02:22.458 --> 00:02:25.873
The main experiment begins with a captured CHECK.

34
00:02:25.873 --> 00:02:29.623
One event XORs its six stored bits before
accepting edge 1.

35
00:02:29.623 --> 00:02:31.918
All sixty-four masks are examined.

36
00:02:31.918 --> 00:02:34.367
The reference image is unauthorized.

37
00:02:34.367 --> 00:02:40.458
The state decoder, source, clock/reset and final
consumer remain trusted.

38
00:02:40.708 --> 00:02:45.450
Mask 111100, hexadecimal 3c, changes 001111 into
110011.

39
00:02:45.450 --> 00:02:51.104
The decoder sees valid RELEASE, bad stays false
and the request commits.

40
00:02:51.104 --> 00:02:53.328
That mask affects four bits.

41
00:02:53.328 --> 00:02:59.332
It lies outside a three-bit claim and inside a
four-bit expanded budget.

42
00:02:59.583 --> 00:03:03.792
The optional bind policy also requires
independent authorization.

43
00:03:03.792 --> 00:03:08.492
It blocks this valid-state witness because the
current image lacks permission.

44
00:03:08.492 --> 00:03:11.602
The model supplies that value from a trusted
harness.

45
00:03:11.602 --> 00:03:18.302
The exercise identifies the missing condition; a
real design must establish its provenance and

46
00:03:18.302 --> 00:03:19.430
integrity.

47
00:03:19.708 --> 00:03:22.964
Select CHECK, mask 1 and no binding.

48
00:03:22.964 --> 00:03:26.529
The result is invalid and commit is false.

49
00:03:26.529 --> 00:03:29.279
Try masks of weight two or three.

50
00:03:29.279 --> 00:03:32.641
Then enter 60, the decimal form of 0x3c.

51
00:03:32.641 --> 00:03:38.141
The displayed code becomes RELEASE and the
request is accepted.

52
00:03:38.141 --> 00:03:41.401
Save this trace beside the state map.

53
00:03:41.667 --> 00:03:47.200
The executed campaign checked every mask from
CHECK and every state-pair distance.

54
00:03:47.200 --> 00:03:51.856
Exactly one of the sixty-four CHECK masks reached
unauthorized RELEASE.

55
00:03:51.856 --> 00:03:56.138
Other four-bit masks can reach WAIT or ERROR and
still remain legal.

56
00:03:56.138 --> 00:04:01.444
No-commit traces therefore must not all be
labeled detected.

57
00:04:01.708 --> 00:04:07.527
Set RELEASE, authorization true, binding true and
mask zero for the positive decoder control.

58
00:04:07.527 --> 00:04:12.023
Lesson 8 separately runs a normal
WAIT-to-CHECK-to-RELEASE transaction.

59
00:04:12.023 --> 00:04:18.543
A decoder control alone does not show the full
controller reaches release or that its transition

60
00:04:18.543 --> 00:04:20.631
conditions are authentic.

61
00:04:20.917 --> 00:04:24.069
The RTL/SVA sketch has not been compiled.

62
00:04:24.069 --> 00:04:30.818
ERROR reachability, output decode failures, scan
access and synthesis recoding are separate

63
00:04:30.818 --> 00:04:31.831
obligations.

64
00:04:31.831 --> 00:04:37.737
Revisit lesson 4 and its separate grant target to
test a corrupted post-decoder output; this

65
00:04:37.737 --> 00:04:40.490
storage-only campaign excludes that target.

66
00:04:40.490 --> 00:04:45.925
A minimum distance of four says nothing about a
faulty CHECK condition choosing a legal next

67
00:04:45.925 --> 00:04:46.349
state.

68
00:04:46.349 --> 00:04:49.395
That is the next lesson.

69
00:04:49.667 --> 00:04:55.777
One six-bit state XOR before edge 1, all
sixty-four masks from CHECK; distance claim

70
00:04:55.777 --> 00:04:57.858
limited to weight below four.

71
00:04:57.858 --> 00:05:01.205
Other logic and reference remain trusted.

72
00:05:01.458 --> 00:05:08.109
Node checked all pair distances and sixty-four
CHECK masks, plus authorized RELEASE decoding.

73
00:05:08.109 --> 00:05:10.689
Normal flow is tested in lesson 8.

74
00:05:10.958 --> 00:05:18.086
No transition, netlist, scan, physical or formal
result follows from this decoder enumeration.