WEBVTT

1
00:00:00.000 --> 00:00:02.577
CHECK-to-RELEASE is a legal arc.

2
00:00:02.577 --> 00:00:05.718
A fault changes the condition selecting it.

3
00:00:05.718 --> 00:00:10.217
Later, a token from transaction 1 is offered for
transaction 2.

4
00:00:10.217 --> 00:00:13.443
Both requests can look structurally normal.

5
00:00:13.443 --> 00:00:18.462
We trace the evidence that should belong to each
accepting event.

6
00:00:18.750 --> 00:00:22.978
A transition relation lists permitted pairs of
states.

7
00:00:22.978 --> 00:00:28.463
WAIT may enter CHECK; CHECK may enter RELEASE on
success or ERROR on failure.

8
00:00:28.463 --> 00:00:32.148
The list can reject a direct WAIT-to-RELEASE
jump.

9
00:00:32.148 --> 00:00:37.212
It cannot establish that the success input itself
was authentic.

10
00:00:37.500 --> 00:00:42.024
In the condition experiment, the current image is
unauthorized.

11
00:00:42.024 --> 00:00:46.034
A single false success decision makes CHECK
choose RELEASE.

12
00:00:46.034 --> 00:00:49.571
The arc checker still recognizes
CHECK-to-RELEASE.

13
00:00:49.571 --> 00:00:53.031
A state-only or arc-only consumer accepts at edge
3.

14
00:00:53.031 --> 00:00:57.808
A fresh authorization condition is needed at the
consumer as well.

15
00:00:58.083 --> 00:01:01.287
The state-jump experiment is separate.

16
00:01:01.287 --> 00:01:05.792
One event after edge 0 sets state to RELEASE
instead of CHECK.

17
00:01:05.792 --> 00:01:09.855
Arc policy moves it to ERROR before the edge-3
request.

18
00:01:09.855 --> 00:01:17.006
This trace shows useful arc coverage, but it does
not remove the forged-condition witness.

19
00:01:17.292 --> 00:01:21.817
Our token carries valid, transaction id and
consumed status.

20
00:01:21.817 --> 00:01:23.980
Current transaction id is two.

21
00:01:23.980 --> 00:01:28.638
A token from prior id one remains stale even if
its valid bit is true.

22
00:01:28.638 --> 00:01:32.631
Freshness requires valid, matching id and not
consumed.

23
00:01:32.631 --> 00:01:38.061
These are ordinary logic fields, not
cryptographic authentication.

24
00:01:38.333 --> 00:01:45.327
For a valid current transaction, trusted
verification creates its token after edge 1.

25
00:01:45.327 --> 00:01:47.840
The request can commit at edge 3.

26
00:01:47.840 --> 00:01:51.470
Acceptance marks it consumed after that edge.

27
00:01:51.470 --> 00:01:59.103
A second request at edge 4 must be denied by the
old consumed state visible before the edge.

28
00:01:59.375 --> 00:02:05.315
The independent monitor also tracks whether an
accepted event has already consumed the one

29
00:02:05.315 --> 00:02:06.508
allowed delivery.

30
00:02:06.508 --> 00:02:08.968
It does not copy the DUT consumed field.

31
00:02:08.968 --> 00:02:14.731
State-only policy in the repeated-request
scenario permits two requests; the second is

32
00:02:14.731 --> 00:02:18.298
unauthorized under this single-delivery contract.

33
00:02:18.583 --> 00:02:22.038
Every trace starts at WAIT and ends at edge 4.

34
00:02:22.038 --> 00:02:26.348
It contains one named fault effect or a repeated
workload.

35
00:02:26.348 --> 00:02:33.122
Condition and stale scenarios select RELEASE
after CHECK; state target jumps after edge 0;

36
00:02:33.122 --> 00:02:36.640
repeat retains RELEASE for the second request.

37
00:02:36.640 --> 00:02:39.814
They are not simultaneous attacks.

38
00:02:40.083 --> 00:02:45.237
The stale experiment begins with valid token id
one and current id two.

39
00:02:45.237 --> 00:02:51.366
This setup includes retained prior evidence and a
permissive decision that trusts it.

40
00:02:51.366 --> 00:02:56.068
Treat it as a protocol-boundary scenario, not one
stored-bit XOR.

41
00:02:56.068 --> 00:03:02.699
Token fields, trusted verification and final
grant remain unfaulted in the bound-policy tests.

42
00:03:02.958 --> 00:03:08.823
SCFI incorporates control signals and execution
history in a hardened next-state function.

43
00:03:08.823 --> 00:03:14.272
Our plain token example teaches the distinction
but does not implement SCFI or inherit its

44
00:03:14.272 --> 00:03:16.343
probabilistic guarantees.

45
00:03:16.625 --> 00:03:20.728
Select condition and arc policy, with
authorization false.

46
00:03:20.728 --> 00:03:25.856
At edge 3, RELEASE and commit are true while the
independent reference is false.

47
00:03:25.856 --> 00:03:30.295
Change policy to bound; there is no valid current
token, so no commit.

48
00:03:30.295 --> 00:03:36.471
Next choose stale and inspect tokenId=1 beside
id=2.

49
00:03:36.750 --> 00:03:40.847
For the repeated request, set authorization true.

50
00:03:40.847 --> 00:03:45.922
State-only policy accepts edges 3 and 4; bound
accepts only edge 3.

51
00:03:45.922 --> 00:03:50.181
Bound checks authorization history, not arc
legality.

52
00:03:50.181 --> 00:03:56.357
An authorized state jump therefore commits under
bound but is rejected under arc.

53
00:03:56.357 --> 00:04:02.719
In the arc trace, edge 1 can show grant before
the update enters ERROR; the request begins at

54
00:04:02.719 --> 00:04:06.235
edge 3, so that earlier grant is not an
acceptance.

55
00:04:06.235 --> 00:04:10.764
All these cases have separate executed
assertions.

56
00:04:11.042 --> 00:04:16.739
The normal positive transaction follows WAIT,
CHECK and RELEASE and commits once.

57
00:04:16.739 --> 00:04:21.373
Fault recovery is not required to retrace an
entirely unfaulted path.

58
00:04:21.373 --> 00:04:27.294
A product may legitimately recover after an
error, but the recovery policy must establish

59
00:04:27.294 --> 00:04:31.276
fresh authorization before a later sensitive
acceptance.

60
00:04:31.542 --> 00:04:33.163
The sketch is uncompiled.

61
00:04:33.163 --> 00:04:38.459
Token storage integrity, id wraparound, abort,
reset and concurrent transactions are excluded

62
00:04:38.459 --> 00:04:38.782
here.

63
00:04:38.782 --> 00:04:43.755
A real transaction-binding scheme needs enough
identity to prevent collisions during its

64
00:04:43.755 --> 00:04:44.789
retention window.

65
00:04:44.789 --> 00:04:48.141
Recovery and liveness need separate properties.

66
00:04:48.141 --> 00:04:52.710
Lesson 9 applies similar protocol reasoning to
configuration writes.

67
00:04:53.000 --> 00:04:53.692
Edges 0.

68
00:04:53.692 --> 00:04:53.762
.

69
00:04:53.762 --> 00:04:59.316
4; separate condition force, state substitution,
stale-token setup and repeated workload.

70
00:04:59.316 --> 00:05:03.743
Tokens, verifier and final grant are trusted in
bound-policy cases.

71
00:05:04.000 --> 00:05:09.246
Node ran ten bound-policy controls plus
forged-condition, stale and repeated-acceptance

72
00:05:09.246 --> 00:05:12.313
witnesses; normal authorized flow commits once.

73
00:05:12.583 --> 00:05:17.491
No SCFI, id-wrap, multi-transaction or physical
assurance is established.

74
00:05:17.491 --> 00:05:19.652
Token fields remain trusted.