Unix forever!

DSR enhanced security and "formal verification" course

Here we are quickly going through the rabbithole of thoughts that caused so much pain to almost all software language and compiler architects over the last decades.

TLA+ - the T stands for "Temporal Logic"

What famous Leslie Lamport's TLA+ verifier is all about: Temporal Logic:

Allen's temporal logic "Interval Algebra'

https://www.researchgate.net/publication/373590095_Standpoint_Linear_Temporal_Logic

https://en.wikipedia.org/wiki/Allen's_interval_algebra

In fact, it's talking about Gantt Diagrams: https://www.gantt.com/ge/

Flows can be visualized with highly sophisticated Graphviz, written in pure C:

Playground: https://graphviz.org/Gallery/neato/process.html
http://magjac.com/graphviz-visual-editor/

graph G {
    fontname="Helvetica,Arial,sans-serif"
    node [fontname="Helvetica,Arial,sans-serif"]
    edge [fontname="Helvetica,Arial,sans-serif"]
    layout=neato
    run -- intr;
    intr -- runbl;
    runbl -- run;
    run -- kernel;
    kernel -- zombie;
    kernel -- sleep;
    kernel -- runmem;
    sleep -- swap;
    swap -- runswap;
    runswap -- new;
    runswap -- runmem;
    new -- runmem;
    sleep -- runmem;
}

Talking philosophically: What relation is there between this diagram and the "Rabbit - Elephant - in the fridge" example timeline? -> Go forward, come back!

Thinking about your ***free time*** in SQL

PostgreSQL on DBFiddle: https://dbfiddle.uk/lvn7uD7I
void printInts(List<int> x) => print(x);

https://www.postgresql.org/docs/current/rangetypes.html

Example: Hotel reservations and overlapping bookings

https://hashrocket.com/blog/posts/postgresql-daterange-and-efficient-time-management

Fun example: Rabbit and Elephant in a fridge

Q: How you get a rabbit into a fridge?

A: Simple: Door open, Rabbit in, Door close, in short: Do-Ri-Dc

Q: How do you get an elephant into the fridge?

A: Door open, rabbit out (because the elephant may step on the poor rabbit), elephant in: Do-Ro-Ei-Dc

Now we do it "multi threaded" on two interleaving "Gantt" timelines:

1
2
3
4
5
         Do----Ri-Dc   (process #1)
Do-Ro-Ei----Dc         (process #2)
===================>  (the timeline!)
Do-Ro-Ei-Do-Dc-Ri-Dc   (here the algorithm breaks!)
         ^^^^^             

Wasn't thread-safe, obviously! Let's file a bug. How would you make it "thread safe"?

Q: What is "atomicity". What's the correspondence in SQL?

That's virtually is what Leslie Lamport's TLA+ verifier is all about and what you can learn in either Hillel's courses: https://www.dabeaz.com/tla.html or directly in Leslie Lamport's excellent TLA+ course on YouTube: https://youtube.com/@tlavideocourse8540/videos

For me as philosopher it's just one more mental model to play with. Notation of Temporal Logic is the other problem. There are almost no standards in that area.

Moving rabbit and elephant from one fridge to the other

To the free TLA+ online book: https://www.learntla.com/

Learn TLA+

Conceptual Overview
To justify the value of TLA+, lets talk about how its useful, and how its different from programming languages.

Imagine were building a wire transfer service for a bank. Users can make transfers to other users. As a requirement, we dont allow any wires that would overdraft the users account, or make it go below zero dollars. At a high level, the could would look like this:

def transfer(from, to, amount)
  if (from.balance >= amount) # guard
    from.balance -= amount;   # withdraw
    to.balance += amount;     # deposit
This would satisfy the requirement: if you try to transfer more than you have, the guard prevents you.

Now consider two changes:

Users can start more than one transfer at a time.

Transfer steps are nonatomic. One transfer can start and (potentially) finish while another transfer is ongoing.

Neither change by itself causes a problem. But both of them together leads to a possible race condition:

Alice has 6 dollars in her account, and makes two transfers to Bob. Transfer X is for 3 dollars, and transfer Y is for 4 dollars.

Guard(X) runs. Because 3 < 6, we go on to Withdraw(X).

Before Withdraw(X) happens, Guard(Y) runs. Because 4 < 6, we go on to Withdraw(Y).

Both withdrawals run, taking 7 dollars out of Alices account and leaving her with -1.

If Withdraw(X) happens before Guard(Y), then theres no problem; transfer Y will simply fail. Race conditions like this are fundamentally rare: most of the time, the program will behave as expected and maintain our properties. Its only in very particular orderings of events that we have a bug. Thats why concurrency errors are so hard to find.

Thats also why theyre hard to fix. Imagine if we added a third feature, say a lock in the right place, to fix the bug. Does the issue go away because weve solved it, or because weve made it rarer? Without being able to explore the actual consequences of the designs, we cant guarantee weve solved anything.

The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirement and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it cant, we can be more confident that were correct.

Structure
So theres three parts to the conceptual framework of TLA+.

First, we need to describe the system and what it can do. This is called the specification, or spec. Our design might look like this:

We have a set of accounts. Each account has a number, representing the balance.

Any account can attempt to transfer any amount of money to any other account.

A transfer first checks if there are sufficient funds. If there are, the amount is subtracted from the first account and added to the second.

Transfers are nonatomic. Multiple transfers can happen concurrently.

The specification has a set of behaviors, or possible distinct executions. For the spec to be correct, every behavior must satisfy all of our system requirements, or properties. No account can overdraft is an example property, and is violated if theres a behavior of the spec has a state where an account has a negative balance. It doesnt matter if all of the other possible behaviors dont have overdrafts. Were looking for rare design error, so just one violation is enough.

Note

No account can overdraft is an invariant property, which is one that must be true of every single state of every single behavior. There are other, more advanced properties, like liveness and action properties, which well cover in time.

Once weve written a spec and properties, we feed them into a model checker. The model checker takes the spec, generates every possible behavior, and sees if they all satisfy all of our properties. If one doesnt, it will return an error trace showing how to reproduce the violation. There are a couple different model checkers for TLA+, but the most popular one is TLC, which is bundled with the toolbox. Unless I say otherwise, when I talk about model checkers Im referring to TLC.

Now we cant check every possible behavior. In fact theres an infinite number of them, since we can also add more accounts and transfers to the system. So we instead check all the behaviors under certain constraints, such as all behaviors for three accounts, of up to 10 dollars in each account, and two transfers, of up to 10 dollars in each transfer. We call this set of runtime parameters, along with all the other model checker configuration we do, the model.

Note

This means that a passing model doesnt guarantee the spec is correct. Maybe theres an error that only appears with larger parameters. But empirically, in specification weve found that most errors appear with very small scopes: if a system works with 3 workers, itll probably also work with 25 workers.

Specifications
So what does this all look like in practice? Lets present a spec for wire transfers, first with hardcoded parameters and then with model-parameterizable ones.

---- MODULE wire ----
EXTENDS TLC, Integers

People == {"alice", "bob"}
Money == 1..10
NumTransfers == 2

(* --algorithm wire
variables
  acct \in [People -> Money];

define
  NoOverdrafts ==
    \A p \in People:
      acct[p] >= 0
end define;

process wire \in 1..NumTransfers
variable
  amnt \in 1..5;
  from \in People;
  to \in People
begin
  Check:
    if acct[from] >= amnt then
      Withdraw:
        acct[from] := acct[from] - amnt;
      Deposit:
        acct[to] := acct[to] + amnt;
    end if;
end process;
end algorithm; *)

====

So learning another language, notation, compiler, gui? Nope: You will very soon learn, that you can do it easily in any other language too! And you will learn, that you will have so simplify, to strip off many features of your beloved programming language to make things ***verifyable***. Modern languages are bloated, overloaded -feature wise.

Thinking about the rabbit example in TLA+

Q: What are the constraints in the rabbit and elephant example?

  • Were they implicit or explicit?
  • How do we express these constraints in TLA+?
  • Can we see the fridge as bank account? How?
  • How do we "withdraw" Rabbit and Elephant from the fridge?
  • Where are they "deposited" if they are not in the fridge?

Q: Do you now see the parallels?

  • How would you formulate the Rabbit problem in TLA+?

Q: Obviously TLA+ permutates states: process wire \in 1..NumTransfers

  • What "state" can the fridge be in?
  • How many processes do we / can we have?

Q: Where did the "timeline thinking" disappear to? Hasn't Leslie Lamport forgotten something?

Q: Can we permutate the processes in Rabbit example?

  • How many processes are there? Let's write them all down:
  1. Do-Ri-Dc
  2. Do-Ei-Dc (here a constraint has to be set: Elephant never step on Rabbit!)
  3. Do-Ro-Ei-Dc (Lucky Rabbit, constrained fulfilled!)
  4. Do-Ro-Dc (trivial, that the Rabbit also can be taken out of the fridge?)
  5. Do-Eo-Dc (sure ...)
  6. ...

Q: Have we gotten all processes right?

  • What is with time delays? State "Do" and nothing happens?
  • Do we have to reformulate our problem?

State "Do" - Time starts ... - ... fridge empty ... still empty ... still empty ...

And then another process finds the Door in "state opened" and quickly puts the Elephant in? ... with "Dc" pending, time delayed ...

And then another process wants to put the Rabbit in, too? Note: Elephant is in the door, but the process was't completed, the door is not yet closed.

Q: Is the Rabbit allowed to step on the Elephant? A: Yes! Obviously no harm!

How we do formulate that as constraint? Is that constaint necessary?

Q: Do we have to insert checks for "Do" and "Dc" states?

Q: Would this solve our problem?

Q: Would adding a check for "if there is something in the fridge and who" help?

Q: What if that check is time delayed?

Q: Do we need a guard or a sentinel? (in german "Wächter")

  • Another lock before the "Dc" locked door?
  • Do we need two doors? Or three? Would 100 doors solve that problem?

Q: What about a ticket automat? Rabbit, Elephant need to draw a ticket first?

  • What's a ticket lock? Does e.g. Rust have a ticket lock? What does the "borrow-checker" internally do?

Q: What processes are allowed when the Elephant is in the fridge?

Q: What processes are allowed when the Rabbit is in the fridge?

Q: What processes are allowed when Elephant first - and then Rabbit - then both are in the fridge?

Q: Can we make a "rules" table, which processes are allowed and when? Refering to

1
2
3
Fridge "empty": Processes allowed: Rabbit in, Elephant in 
Fridge with Elephant in: Rabbit in
Fridge with 

So a flow graph like in https://graphviz.org/Gallery/neato/process.html is not sufficient. We need conditioned flows:

1
2
3
4
State A fulfilled, B fulfilled -> Process 1;
State A unfulfilled, B fulfilled -> Process 2; then Process 1;
...
...

Means: We need a "Transition State Table" of the form:

https://github.com/gbmhunter/FunctionPointerStateMachineExample/

1
2
3
4
5
6
7
8
static stateTransMatrixRow_t stateTransMatrix[] = {
    // CURR STATE  // EVENT              // NEXT STATE
    { ST_IDLE,     EV_BUTTON_PUSHED,     ST_LED_ON  },
    { ST_LED_ON,   EV_TIME_OUT,          ST_LED_OFF },
    { ST_LED_ON,   EV_BUTTON_PUSHED,     ST_IDLE    },
    { ST_LED_OFF,  EV_TIME_OUT,          ST_LED_ON  },
    { ST_LED_OFF,  EV_BUTTON_PUSHED,     ST_IDLE    }
};

Q: Before we start: Are "Do" - Door open and "Dc" - Door close states or processes? Or both?

...
...
...

Can you imagine that most programmers are confused by this?

The new Python "pattern matching" syntax

https://peps.python.org/pep-0622/

def make_point_3d(pt):
    match pt:
        case (x, y):
            return Point3d(x, y, 0)
        case (x, y, z):
            return Point3d(x, y, z)
        case Point2d(x, y):
            return Point3d(x, y, 0)
        case Point3d(_, _, _):
            return pt
        case _:
            raise TypeError("not a point we support")

Another example:

1
2
3
4
5
6
7
8
9
match something:
    case 0 | 1 | 2:
        print("Small number")
    case [] | [_]:
        print("A short sequence")
    case str() | bytes():
        print("Something string-like")
    case _:
        print("Something else")

Now we introduce guards or sentinels, TLA+ constraints

1
2
3
4
5
6
7
8
9
match input:
    case [x, y] if x > MAX_INT and y > MAX_INT:
        print("Got a pair of large numbers")
    case x if x > MAX_INT:
        print("Got a large number")
    case [x, y] if x == y:
        print("Got equal items")
    case _:
        print("Not an outstanding input")

Python obviously has a built-in type verifier:

1
2
3
4
5
6
7
8
9
def classify(val: Union[int, Tuple[int, int], List[int]]) -> str:
    match val:
        case [x, y] if x > 0 and y > 0:
            return f"A pair of {x} and {y}"
        case [x, *other]:
            return f"A sequence starting with {x}"
        case int():
            return f"Some integer"
        # Type-checking error: some cases unhandled.

Notation standards in math, sciences and computer sciences

The complete overview of math notation on 10 pages:

http://www.tug.org/texshowcase/cheat.pdf
https://en.wikipedia.org/w/index.php?title=Glossary_of_mathematical_symbols

New Standpoint Temporal Logic notation

https://www.researchgate.net/publication/373590095_Standpoint_Linear_Temporal_Logic

What's a "standpoint"? A context. You you see the world is your context. It's how you interpret events. Like environment variables in programming, in containers, in machine code execution stacks. Nothing more!

Thinking in "timeline - events - rules (constraints)" model

These are the upcoming new patterns in computing. Why? The do scale on parallel and distributed computing!

There is a new software architecture upcoming, which has a very quite different approach of "seeing, interpreting the world": http://event-db.com

ECS: https://en.wikipedia.org/wiki/Entity_component_system
CQRS: https://en.wikipedia.org/wiki/Command-Query-Responsibility-Segregation
Event Sourcing: https://en.wikipedia.org/wiki/Command-Query-Responsibility-Segregation

Computer science metanotation (CSM)

https://cs.stackexchange.com/questions/83770/help-understand-the-notation

Guy Steele: https://youtube.com/watch?v=7HKbjYqqPPQ
https://youtube.com/watch?v=dCuZkaaou0Q&t=1h1m0s

Back to last lesson - https://rentry.co/DSRsecuritycoursepart8 Next lesson: https://rentry.co/DSRsecuritycoursepart10

Edit
Pub: 27 Jun 2024 09:21 UTC
Edit: 12 Jul 2024 09:08 UTC
Views: 226