https://github.com/freedomofpress/securedrop-client/issues/1617

.gitignore

states/

*.dot
*.out

README.md

securedrop-client#1617 Unify [Draft]Reply objects

Read this gist in this order for maximum comprehensibility:

File	Description
README.md	This readme
Reply.mmd	"Hand-drawn" state diagram for a proposed Reply state machine
Reply.cfg	TLA+ configuration for the Reply module modeling this state machine
Reply.tla	TLA+ specification
Reply.tla.dot.png	Graphviz rendering of Reply.tla, to check visually against Reply.mmd
Reply.tla_liveness.dot.png	Graphviz rendering of TLA+'s own proof of the Termination liveness property

TODO (and findings)

• Check recovery modes (e.g., DownloadFailed → Downloaded at the storage versus controller/GUI layers)
  • Recovery/retry logic is internal to the pending state represented by a given ApiJob implementation. Therefore, failure states are terminal.
    • Ideally these states would be captured definitively in the model-level state at the storage layer and then propagated up for the controller and GUI layers to filter and handle as they see fit.
• Add deletion
  • Deletion can happen at any time!
  • Actually, there is a hierarchy:
    • Local deletion exits the "alive" state machine and transitions to "dead".
    • Remote deletion supervenes on local deletion and transitions to "gone" (that is, actually deleted) whether exiting the "alive" or the "dead" state machine.
• Model states as sets and add invariants/properties
  • TLA+'s real magic lies in explicating implicit state machines, where it's useful to be able to define invariants to test expected states.
  • Since we already have an explicit state machine, however, and since all Replys are independent, we can define properties directly, without modeling individual Reply's paths through the states (sets).
  • We can see this because Reply.tla_liveness.dot.png is identical (mod colors) to Reply.tla.dot.png: TLA+'s liveness proof of our state machine matches the state machine itself.

Insights

The Reply object is subject to intersection of two independent processes in which client-side intent must be reflected regardless of server-side result:

1. Even if a reply fails to send, is rejected, etc., it still exists and has a status.
   • Star-related operations could be implemented in this way but need not be.
2. Both local and remote deletion may happen at any time, and remote deletion supervenes on local deletion.
   • All client-side operations on sources and conversations are subject to this property. Therefore all client-side objects—including their persistent representations and their GUI presentations—should consistently reflect these "alive" and "dead" states.

This model therefore turns out to be a refinement of a general pattern for processing commands, where:

1. The Client sends document messages and command messages.
2. The Server returns document messages and event messages.
3. Both Client and Server are idempotent receivers.

These patterns would give the Client more resilience as an occasionally-connected application. That's out of the scope of this redesign effort, and it ought to depend on the findings of the current E2EE research effort.

Makefile

DOT=$(wildcard *.dot)
PNG=$(DOT:.dot=.dot.png)

.PHONY: all

all: $(PNG)

%.dot.png: %.dot Makefile
	dot -Tpng $< > $@

Reply.cfg

SPECIFICATION Spec
PROPERTY Termination

Reply.mmd

Reply.tla

Adapted from <https://learntla.com/topics/state-machines.html>.

---- MODULE Reply ----
EXTENDS TLC
VARIABLE state
vars == <<state>>

\* Dead (to us): we've deleted it locally, but we have to keep it around until it's confirmed
\* deleted remotely too.
Dead == {"DeletedLocally"}

AliveTerminalStates == {
    "Ready",

    "DecryptionFailed",
    "DownloadFailed",
    "SendFailed"
}

TerminalStates == AliveTerminalStates \union Dead

\* Alive: we haven't deleted it locally yet, nor has it been deleted remotely.
AliveStates == AliveTerminalStates \union {
    "SendPending",
    "Sending",

    "DownloadPending",
    "Downloading",
    "Downloaded"
}

\* Gone: either it was dead and now it's gone (confirmed deleted remotely); or it was just
\* deleted remotely.

States == AliveStates \union Dead

TopDown == [Alive |-> AliveStates] @@ [s \in States |-> {}]

RECURSIVE In(_, _)
In(s, p) ==
    \/ s = p
    \/ \E c \in TopDown[p]:
        In(s, c)

Trans(from, to) ==
    /\ In(state, from)
    /\ state' = to

Init ==
    \/ state = "SendPending"  \* type == "outgoing"
    \/ state = "DownloadPending"  \* type == "incoming"

Next ==
    \* Local deletion can occur at any time:
    \/ Trans("Alive", "DeletedLocally")

    \* Outgoing reply (we're sending):
    \/ Trans("SendPending", "Sending")  \* in SendReplyJob
    \/ Trans("Sending", "SendFailed")
    \/ Trans("Sending", "Ready")  \* sent

    \* Incoming reply (someone else sent; we're downloading):
    \/ Trans("DownloadPending", "Downloading")  \* in DownloadReplyJob
    \/ Trans("Downloading", "DownloadFailed")
    \/ Trans("Downloading", "Downloaded")
    \/ Trans("Downloaded", "DecryptionFailed")
    \/ Trans("Downloaded", "Ready")  \* decrypted

    \* Don't deadlock on terminal states.
    \/ /\ state \in TerminalStates
       /\ UNCHANGED state

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)

\* Prove that the machine reaches a terminal state.  By contrast,
\* <>[](state \in AliveTerminalStates) does *not* hold, and TLA+ will warn us that the path (e.g.)
\* Send --> SendPending --> DeletedLocally violates it.
Termination == <>[](state \in TerminalStates)
====

Reply.tla.dot.png

Reply.tla_liveness.dot.png

It seems to me that it should be possible and would be interesting to check properties like:

• new incoming/outgoing replies eventually move to a terminal state

I think this one is an example of temporal property, and that it would be part of the liveness part of the specification. I'm looking at the Liveness section of https://lamport.azurewebsites.net/video/video9b-script.pdf, but I'm not seeing yet how the property above could be expressed within the spec we have. 💭

---

Thinking aloud: it seems to me that proving that an outgoing message eventually moves to a terminal state would require including the entity that sends the message in the described system.

@gonzalo-bulnes in https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434209#gistcomment-4434209:

Note that the Mermaid diagram supports identifying multiple terminal states:

Thanks! Fixed in 4802be8.

---

https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434211#gistcomment-4434211:

Am I reading the spec correctly? "Given an NewOutgoingReply the state machine never stops (read: never gets in an invalid state)", idem for any given NewIncomingReply. @cfm

Not quite! Read—

Spec ==
    /\ \/ NewOutgoingReply
       \/ NewIncomingReply
    /\ [][Next]_state

—as a refinement of the default—

Spec ==
    /\ Init
    /\ [][Next]_state

—with two possible Init states. So Spec begins at (either) Init and then traverses all possible transitions of state defined by Next.

---

https://gist.github.com/cfm/2ca373e7ac5e5397550d7db98289dc3d?permalink_comment_id=4434224#gistcomment-4434224:

It seems to me that it should be possible and would be interesting to check properties like:

• new incoming/outgoing replies eventually move to a terminal state

I think this one is an example of temporal property, and that it would be part of the liveness part of the specification. I'm looking at the Liveness section of https://lamport.azurewebsites.net/video/video9b-script.pdf, but I'm not seeing yet how the property above could be expressed within the spec we have. 💭

Right; this is too abstract. For that I'd need to:

1. model each state as a set;
2. model the progression of a NewOutgoingReply and a NewIncomingReply through those sets; and
3. define invariants like "no reply is ever in two states at once" and properties like "all replies eventually reach a terminal state".

Next week!

Thinking aloud: it seems to me that proving that an outgoing message eventually moves to a terminal state would require including the entity that sends the message in the described system.

Isn't that two different models to prove two different things in two different components at two different layers? :-)

1. "Every outgoing message moves to a terminal state."
2. "The sending queue returns success or failure for every message enqueued to it."

@gonzalo-bulnes, see the latest version of this gist for:

1. an Init refactored for clarity;
2. a liveness property (Termination) for this explicit (now hierarchical!) state machine; and
3. my interpretation of why we needn't model further properties in this case, since (a) the state machine is explicit and (b) all instances (Replys) are independent. By contrast, we would need more properties for the implicit and intradependent state machine of full Client‒Server interactions—or even just two mailboxes.

I'm reconsidering my point (3) above. Based on these findings, I think it would still be worth it to model the composition of—

1. this Reply state machine;
2. the SendReplyJob and DownloadReplyJob that operate on it directly; and
3. the deletion operations that affect it indirectly

—precisely because together they constitute just such an implicit and intradependent state machine. I'll consider this a prerequisite of implementing this change if my proposal for it (forthcoming next week) is approved.

👀