State the consistency property provided to clients of AFS.
Problem 2 (Falcon)
In Falcon, a spy has the power to kill a component so that it can be sure that
that component has failed. Is it possible for a spy that satisfies Falcon's
assumptions to kill a component, yet still have that component continue to
execute instructions on its CPU? If yes, why is this OK, and if no, what
would be the negative consequence of the component continuing to execute
instructions?
Problem 3 (FARSITE)
In Farsite, each Byzantine-fault-tolerant state machine computes the time as
follows. It gathers time estimates from each of the $3f+1$ members of the BFT
group, and considers the time to be the $f+1$st largest member time. What could
go wrong if it considered the time to be the largest member time? What could
go wrong if it considered the time to be the smallest member time?
Problem 4 (Seeing is Believing)
Construct a set of transactions that satisfies
∃ e . ∀ T ∈ 𝓣 . CTSI(T, e)
but
¬ ∀ T ∈ 𝓣, e . CTSER(T, e) .
Show the execution e and the witnesses s, sp for each T that establish CTSI.
Argue why CTSER is unsatistfiable.
You may assume any initial state; that is, the initial state can be implied by the values read in the transactions.