Logics

Week 0xE

Announcements

• Last Lecture
  • Security topics unrelated to crypto
  • Some automata theory
• Action items
  • heap_t due now
  • BTCinC final is out

Today

• Threat and Threat Models
• (Trace) Properties
• Kripke Structures
• Linear Temporal Logic
• Büchi Automata
  • DFAs
  • Safety & Liveness
• CIA Triad

Threat

• “Security” is incomplete as a concept.

  • What is secure?
  • For whom is the ‘what’ secure?
  • From whom is the ‘what’ secure?

Bitcoin

• Bitcoins are secure.
• For all senders and receivers the ownership is secured.
• From any third party the doublespending is secured.

Limitations

• Can a third party tell who uses the service?
• Can a third party tell when coins are being sent?
• Can a third party tell the amount of the transaction?

Models

Use threat modeling:

• Description of the subject to be modeled
• Assumptions that can be checked or challenged
• Potential threats to the system
• Actions that can be taken to mitigate each threat
• A way of validating the model and threats

Read more: OWASP.org

Informally	Formally
What?	Description of the subject to be modeled
For whom?	A way of validating the model and threats
From whom?	Potential threats to the system
Any limitations?	Assumptions that can be checked
How?	Actions that can be taken to mitigate each threat

BTC

Informally	Formally
What?	Currency
For whom?	An economy with internet access
From whom?	Fraud, central authority, surveillance
Any limitations?	Public ledger
How?	bchain.html

How?

We can instead proceed in four steps.

1. Diagram: What are we building?
2. Identify threats: What could go wrong?
3. Mitigate: What are we doing to defend against threats?
4. Validate: Have we acted on each of the previous steps?

Diagram

Threats

• What if?
  • Two entities have the same private key?
  • Dishonest nodes have more compute power?
  • Internet goes down?

Mitigate

• Well…
  • Keys are ~4096 bit…
  • There are other more lucrative uses of compute than competing with BTC nodes
  • If the internet goes down, coins can’t be spent but persist locally

Validate

• This is new!
• Cryptobook uses “Attack Games”
• We explore “digital signature”

Cryptobook:

We give the adversary the power to mount a chosen message attack, namely the attacker can request the signature on any message of his choice. Even with such power, the adversary should not be able to create an existential forgery, namely the attacker cannot output a valid message-signature pair \((m, \omega)\) for some new message \(m\).

Cryptobook:

Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:

• The challenger runs \((pk, sk) \leftarrow \mathcal{G}()\) (private signing key, public verifying key) and sends \(pk\) to \(\mathcal{A}\).

Cryptobook:

Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:

• \(\mathcal{A}\) queries the challenger several times. For \(i = 1, 2, \dots\), the \(i^{th}\) signing query is a message \(m_i \in \mathcal{M}\). Given \(m_i\), the challenger computes \(\sigma_i \leftarrow \mathcal{S}(sk, m_i)\), and then gives \(\sigma_i\) to \(\mathcal{A}\).

Cryptobook:

Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:

• Eventually \(\mathcal{A}\) outputs a candidate forgery pair \((m, \sigma) \in \mathcal{M} \times \Sigma\).

Cryptobook:

Attack Game 13.1 (Signature security). For a given signature scheme \(\mathcal{S} = (\mathcal{G}, \mathcal{S}, \mathcal{V})\), (generate, sign, verify) defined over \((\mathcal{M}, \Sigma)\), (messages, signatures), and a given adversary \(\mathcal{A}\), the attack game runs as follows:

• We say that the adversary wins the game if the following two conditions hold:

\[ \mathcal{V}(pk, m, \sigma) = \text{accept} \]

Techniques

• Define the scope and depth of analysis.
• Gain a visual understanding of what you’re threat modeling.
• Visually model the attack possibilities.
• Identify threats.
• Document of missing or weak security controls.

Scope

• Determine stakeholders
  • Who uses the service?
  • Who provides the service?
  • Who benefits from the service?
  • Who does not benefit from the service?

Scope

• Who can answer these questions?
  • Are they the same or different people?
  • Should you do this by yourself?
  • What do you do if you need help?

Visuals

digraph block_chain {
  rankdir=TD;
  bgcolor="#191919";

  node [
      fontcolor = "#ffffff",
      color = "#ffffff",
      shape=record
  ]

  edge [
      color = "#ffffff",
      fontcolor = "#ffffff"
  ]

  1 [label="{h(prev)|<here> h(root)}|{time|nonce}"]
  0 [label="{<there> h(prev)|<here> h(root)}|{time|nonce}"]
  2 [label="{<there> h(prev)|<here> h(root)}|{time|nonce}"]
  merkle [label="{<1> 0x1|h(*0x2,*0x3)}|{0x2|h(*0x4,*0x5)}|{0x3|h(*0x6,*0x7)}|{0x4|h(*0x8,*0x9)}|{0x5|h(*0xA,*0xB)}|{0x6|<6> h(G,C,2)}|{0x7|<7> h(A,G,4)}|{0x8|<8> h(A,B,1)}|{0x9|<9> h(B,C,2)}|{0xA|<A> h(C,D,3)}|{0xB|<B> h(F,A,7)}"]
  
  heap [shape=record, label="{send|recv|amnt}|{<e> G|C|2}|{<f> A|G|4}|{<a> A|B|1}|{<b> B|C|2}|{<c> C|D|3}|{<d> F|A|7}"]

  1 -> 0:there
  0 -> merkle:1
  0 -> 2:there
  merkle:7 -> heap:f
  merkle:6 -> heap:e
  merkle:B -> heap:d
  merkle:A -> heap:c
  merkle:9 -> heap:b
  merkle:8 -> heap:a

}

Threats

• What if?
  • Someone changes (G,C,2) to (G,C,3)
  • G submits a second (G,G,2) next block
  • G loses their private key?

Document

• https://bitcoin.org/bitcoin.pdf
• https://github.com/bitcoin/bitcoin

Traffic light

• Diagram: What are we building?
• Identify threats: What could go wrong?
• Mitigate: What are we doing to defend against threats?
• Validate: Have we acted on each of the previous steps?

Today

• ✓ Threat and Threat Models
• (Trace) Properties
• Kripke Structures
• Linear Temporal Logic
• Büchi Automata
  • DFAs
  • Safety & Liveness
• CIA Triad

Properties

• An security policy may have properties.
• These security policies are distinct from the what? of a threat model
• Rather the security policy is the how? of a threat model

A security policy could have the property of being secure if the threats of a threat model are mitigated

Trace Properties

• I think of properties in terms of traces
• A trace is the sequence of states through which a system passes over time.
  • A sequence is an ordered collection.
  • A state is the configuration of a system at some specific time point.
  • A system implements the security policy.
  • Emphasize the notion of over time. Traces are time-based.

Traffic Light

• Think of a traffic light.
  • In what states may a traffic light be?
  • In what sequence may these states occur?
  • Does a traffic light implement a security policy
  • Do traffic lights change over time?

State Machine

• A traffic light is a state machine.

A state machine is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time.

• Often called “FSM” (finite state machine)
  • I don’t have a hot new start-up selling infinite states.

A Trace

• We can denote the state of a traffic light by the lit color. (“Wow this class is lit.”)
• A trace may appear as:

trace = [
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW"
]

Examples

• Let’s review some traces and see if they are from a traffic light system that is operating properly.

summarize = lambda t : "".join([s[0] for s in t])

• Can also express traces as e.g. RGYRGYRGY

Start

• Does starting state matter?

trace = [
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW"
]

trace = [
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_"
]

trace = [
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___"
]

End

• Does ending state (terminating state) matter?

trace = [
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW"
]

trace = [
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_"
]

trace = [
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___"
]

Length

• Does length (or perhaps size) matter?

trace = [
    "YELLOW",
    "RED___"
]

trace = [
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW"
]

trace = [
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___",
    "GREEN_",
    "YELLOW",
    "RED___"
]

Unique

• Does number of unique states matter?

trace = [
    "YELLOW",
]

trace = [
    "GREEN_",
    "YELLOW"
]

trace = [
    "RED___",
    "GREEN_",
    "YELLOW"
]

Order

• Does order matter?

trace = [
    "GREEN_",
    "RED___",
    "YELLOW"
]

trace = [
    "RED___",
    "YELLOW",
    "GREEN_"
]

trace = [
    "RED___",
    "GREEN_",
    "YELLOW"
]

Sets of Traces

Note

A trace property is a set of traces.

• Say, variable “property” is a list of traces.
  • Should be a set.

  property[0] = ["GREEN_"]
  property[1] = ["YELLOW"]
  property[2] = ["RED___"]
  property[3] = ["GREEN_", "YELLOW"]

System Properties

• Say a system “satisfies” property \(p\) if all possible traces produced by a system are in the property.
• This may be an infinite number of traces or include traces of infinite length.
• Systems may have (satisfy) more than one property.

On Security

Properties provide a way to answer the “How?” after asking:

• What is secure?
• For whom is the ‘what’ secure?
• From whom is the ‘what’ secure?

Sets of Traces

• A set is an ordered collection of elements (such as sequences).
• A sequence is an ordered collection of elements (such as states).
• A trace property is a set of traces.
• A trace is a sequence of states.

Organization

Example

Enumeration

• Thus far, we enumerated the possible traces.

property[0] = ["GREEN_"]
property[1] = ["YELLOW"]
property[2] = ["RED___"]
property[3] = ["GREEN_", "YELLOW"]

• This is bad. Why?

Specification

• Rather than enumerate, let us specify.

The traffic light property is
    the set of all sequences over precisely the states {"GREEN_", "YELLOW", "RED___"} such that 
        the only state succeeding "GREEN_" is "YELLOW" and
        the only state succeeding "YELLOW" is "RED___" and
        the only state succeeding "RED___" is "GREEN_".

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• Kripke Structures
• Linear Temporal Logic
• Büchi Automata
  • DFAs
  • Safety & Liveness
• CIA Triad

Model Checking

• A Kripke Structure is a tuple that models a state machine.
• Recall:
  • A state machine is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time.
  • Exactly one!

Model Checking

A Kripke Structure is a tuple {S, …} that models a state machine.

• S is a finite set of states
  • Kripke structures only work for finite state machines
  • For the sake of this class, we can imagine infinite states if needed.

Model Checking

A Kripke Structure is a tuple {S, …} that models a state machine.

• For a traffic light, S is: {"GREEN_", "YELLOW", "RED___"}

• For a Bitcoin, it is perhaps the current owner.

  • Many possible, but finite, number of owners.

Model Checking

A Kripke Structure is a tuple {S, I, …} that models a state machine.

• I is a subset of S, we denote this I ⊂ S
  • Any state in I must be a state in S
  • There may be states in S that are not in I
  • These are the possible initial states of the state machine.

Model Checking

A Kripke Structure is a tuple {S, I, …} that models a state machine.

• For a traffic light, I = S {"GREEN_", "YELLOW", "RED___"}

• For a Bitcoin, the initial state is Satoshi Nakamoto’s public key.

Model Checking

A Kripke Structure is a tuple {S, I, …} that models a state machine.

• S is a finite set of states
• I ⊂ S is the set of initial states.

Model Checking

A Kripke Structure is a tuple {S, I, R, …} that models a state machine.

• R is a transition relation over S, we denote this R ⊂ S × S
  • This just means R says whether one state may be transitioned to from another.
  • Same as graph edges (if we take S to be nodes)

Model Checking

• BONUS/CHALLENGE: R is left-total.

Note

A binary relation R ⊂ S × S is left-total if for all elements s of S there exists some ordered pair in R such that the first element of the ordered pair is s.

• R ⊂ S × S is left-total ≔ ∀ s1 ∈ S, ∃ s2 ∈ S such that (s1,s2) ∈ R

Model Checking

A Kripke Structure is a tuple {S, I, R, …} that models a state machine.

• For a traffic light, R is:

{("GREEN_", "YELLOW"),
 ("YELLOW", "RED___"),
 ("RED___", "GREEN_")}

• For Bitcoin, the Cartesian product.

Model Checking

A Kripke Structure is a tuple {S, I, R, …} that models a state machine.

• S is a finite set of states
• I ⊂ S is the set of initial states.
• R ⊂ S × S is a left-total transition relation.

Model Checking

A Kripke Structure is a 4-tuple {S, I, R, L} that models a state machine.

• L is a labeling function over S, we denote this L ⊂ S → ???
  • This just means L provides a way of talking about the states in S
  • We talk about these states using atomic propositions

Atomic Propositions

• Propositions are expressions in propositional, or zeroth order, logic.
• They are simply true or false.
• Atomic propositions are simplest possible form of these logic expressions.
• L ⊂ S → 2^AP

Model Checking

A Kripke Structure is a 4-tuple {S, I, R, L} that models transitions between over atomic propositions AP.

• L is a labeling function over S, we denote this L ⊂ S → 2_AP_
  • Given AP, L tells us whether each is true or false (2 options) for every given state.

Model Checking

A Kripke Structure is a 4-tuple {S, I, R, L} that models transitions and AP.

• For a traffic light, regard AP as the bit encoding of the current state, with perhaps bits encoding “redness”, “yellowness”, and “greenness”
• These happen to be but are not required to be mutually exclusive.

AP

• Or just take a “red” and “green” proposition.
• The easiest way to imagine this is with hexcodes

red    = 0xFF0000
green  = 0x00FF00
yellow = red + green

• Regard a yellow light as a light that is both red and green (after all… it is)

Model Checking

A Kripke Structure is a 4-tuple {S, I, R, L} that models transitions and AP.

• S is a finite set of states
• I ⊂ S is the set of initial states.
• R ⊂ S × S is a left-total transition relation.
• L ⊂ S → 2_AP_ is the labelling relation.

Diagrams

Now that I’ve rigorously defined Kripke Structures, I am willing to tell you they are just diagrams.

• Clarke, Edmund & Grumberg, Orna & Jha, Somesh & Lu, Yuan & Veith, Helmut. (2003). Counterexample-guided abstraction refinement for symbolic model checking. J. ACM. 50. 752-794. 10.1145/876638.876643.

Diagrams

• \(\{S, I, R, L\}\)
  • \(S := \{ S_1, S_2, S_3 \}\)
  • \(I := \{ S_1 \}\)
  • \(R := \{(1,2), (2,1), (2,3), (3,3)\}\)
  • \(L := \{({p,q},1), ({q},2), ({p},3)\}\)

Traffic Light

• \(\{S, I, R, L\}\)

Traffic Light

• \(\{S, I, R, L\}\)
  • \(S := \{ S_1, S_2, S_3 \}\)
    • Denote states as numbered circles.

Traffic Light

• \(\{S, I, R, L\}\)
  • \(S := \{ S_1, S_2, S_3 \}\)
  • \(I := \{ S_1, S_2, S_3 \}\)
    • Denote as incoming arrows

Traffic Light

• \(\{S, I, R, L\}\)
  • Skip to labels
  • Basically have:
    • \(\{r\}\)
    • \(\{g\}\)
    • \(\{r,g\}\)
  • Just use that order.

Traffic Light

• \(\{S, I, R, L\}\)
  • The state names are not meaningful
  • I can make them whatever I want via \(L\)

Traffic Light

• \(\{S, I, R, L\}\)
• We have our transition relation.
• Side-to-top

	R	G	Y
R		x
G			x
Y	x

Traffic Light

• \(\{S, I, R, L\}\)
• Perhaps omit \(I\) denotation.

Acceptance

• We say a trace is accepted if
  • It starts in a start state, and
  • For each new tracepoint, there is an edge.

Acceptance

• R is accepted.

Acceptance

• RG is accepted.

Rejection

• RY is a rejected.
  • No edge from R to Y

Limitations

• Better than enumeration, but…
  • In text is too complex
  • Considering traces is difficult in nontrivial cases.
• We will introduce a better way to write out relations, then look at our Kripke Structures.

TCP

• Consider the “famous” TCP 3-way handshake.

• More

TCP

• State is more complex.
  • Tracking whether SYN and ACK have been received by both client and server.

TCP

• Transitions are more complex.
  • Vs, a light which is red and becomes red.
  • A server is in state, say LISTEN and then transitions to state SYN-RECEIVED.

TCP

• Is this trace accepted?
  1. Client.SYN
  2. Client.SYN x2
  3. Server.SYN
  4. Server.ACK
  5. Client.ACK

TCP

• Server/Client requires SYN initially.
• Server may not ‘SYN’ or ACK until seeing SYN
• Client may not ACK until seeing ACK
• Client must ACK

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• ✓ Kripke Structures
• Linear Temporal Logic
• Büchi Automata
  • DFAs
  • Safety & Liveness
• CIA Triad

neXt and Until

• It often suffices to define two temporal operators:

  • X: “neXt”
  • U: “Until”

• Along with existing logical operators:

  • ¬: “not”
  • ∨: “or”

• Apply these over atomic propositions in AP to describe security.

Composition

With logical negation (not) and disjunction (or) we can generate other logical connectives.

\(p\)	\(q\)	\(\neg p\)	\(p \lor q\)	\(\neg p \lor \neg q\)	\(\neg p \lor \neg q \equiv p \land q\)
True	True	False	True	False	True
True	False	False	True	True	False
False	True	True	True	True	False
False	False	True	False	True	False

Next and Until

Derived Unary

Name	Written:	Meaning	Equivalencies
neXt	X p	p holds in the next time	X p
Future	F p	p holds in some future time	True U p
Global(ly)	G p	p holds future times	¬(True U ¬ p)

Derived Binary

Name	Written:	Meaning	Equivalencies
Until	p U q	p holds unless q, q must hold eventually	p U q
Release	p R q	q holds up to and including when p holds	¬(¬ p U ¬ q)

Special Binary

Name	Written:	Meaning	Equivalencies
Weak until	p W q	p holds up to when q holds	(p U q) ∨ G p
Mighty release	p M q	q holds up to and including when p holds, and p must hold eventually	q U (p ∨ q)

Properties

• Some security properties are about bad things not happening:
  • G \(\neg\) bad
  • Term this “safety”
• Some security properties are about good things happening someday:
  • F good
  • Term this “liveness”

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• ✓ Kripke Structures
• ✓ Linear Temporal Logic
• Büchi Automata
  • DFAs
  • Safety & Liveness
• CIA Triad

Aside

• Büchi Automata are just “DFA” (deterministic finite automata) that aren’t finite.
• They accomplish this through an uninteresting hack.
• DFAs are the first automata taught in theory of computing and automata theory class.
• The follow slides conclude the “sets/graphs/automata” portion of class, among other things.

Finite Automata

Definition

• Term this \(M_1\):

  • States \[ q_n \]

  • Transitions \[ \overset{\{1\}}{\longrightarrow} \]

  • Start state \(q_1\)

  • Accept state \(q_3\)

Process

• Term this \(M_1\):

  • States \[ q_n \]

  • Transitions \[ \overset{\{1\}}{\longrightarrow} \]

  • Start state \(q_1\)

  • Accept state \(q_3\)

• Input
  • Finite bit string
  • \(\{0,1\}^n\)
• Output
  • Boolean or bit
  • \(\{0,1\}\)
• Begin in start
• Read symbol
• Follow edge

’’

• The inital state is \(q_1\).

[] # We'll use a Python list to represent the input.

‘0’

• Find label containing 0 out of \(q_1\).

[0] # We'll use a Python list to represent the input.

‘01’

• Find label containing 1 out of \(q_1\).

[0, 1] # We'll use a Python list to represent the input.

‘011’

• Find label containing 1 out of \(q_2\).

[0, 1, 1] # We'll use a Python list to represent the input.

‘0110’

• Find label containing 0 out of \(q_3\).

[0, 1, 1, 0] # We'll use a Python list to represent the input.

‘01101’

• Find label containing 1 out of \(q_3\).

[0, 1, 1, 0, 1] # We'll use a Python list to represent the input.

‘01101’

• \(M_1\) accepts [0, 1, 1, 0, 1] by ending in \(q_3\)

assert(M_1([0, 1, 1, 0, 1]) # M_1 as a function from bit strings to booleans.

Exercise

• Does \(M_1\) accept [0, 0, 1, 0, 1]?

[0, 0, 1, 0, 1] # M_1 as a function from bit strings to booleans.

Terminology

• We say that:
  • \(A\) is the language of \(M_1\).
  • \(M_1\) recognizes \(A\)
  • \(A = L(M_1)\)
• We note: \[ w \in A \implies \exists i < |w| - 1 : w_i = 1 \land w_{i+1} = 1 \]

w = '01101' # for example
assert('11' in w)

Formal Definition

A finite automaton is formally defined as a 5-tuple:

• \(Q\) A finite, non-empty set of states.
• \(\Sigma\): A finite, non-empty set of input symbols called the alphabet.
• \(\delta\): The transition function, a mapping
  • \(\delta : Q \times \sigma \rightarrow Q\)
• \(q_0\): The initial state, where \(q_0 \in Q\).
• \(F\): A set of accepting states (or final states), where \(F \subset Q\).

Explanation:

• States (\(Q\)): Possible internal configurations - like computer memory.
• Alphabet (\(\Sigma\)): Possible inputs - machine binary or computer I/O.
• Transition Function (\(\delta\)): How the FA’s state is updated on read.
• Initial State (\(q_0\)): This is the state where the automaton begins its operation.
• Accepting States (\(F\)): These determine if the FA outputs \(0\) or \(1\).

Our Example

• \(M_1 = (Q, \Sigma, \delta, q_1, \{q_3\})\)
  • \(Q = \{q_1, q_2, q_3\}\)
  • \(\Sigma = \{0, 1\}\)
• How to express \(\delta\)?

\(\delta=\)	\(0\)	\(1\)
\(q_1\)|	\(q_1\)	\(q_2\)
\(q_2\)|	\(q_1\)	\(q_3\)
\(q_3\)|	\(q_3\)	\(q_3\)

Python

# define q_n as a convenience
q_1, q_2, q_3 = "q_1", "q_2", "q_3"
# define M_1
Q = {q_1, q_2, q_3}
S = {0, 1}
d = {
    q_1 : { 0:q_1, 1:q_2 },
    q_2 : { 0:q_1, 1:q_3 },
    q_3 : { 0:q_3, 1:q_3 }
}
M_1 = (Q,S,d,q_1,{q_3})

Strings/Languages

• A string is a sequence of letters \(\Sigma^n\)
• A language is a set of strings.
• The empty string is zero length \(\Sigma^0\)
• The empty language is the empty set \(\varnothing\) We previously used the term “trace” the way DFAs use “string”.

We note that the empty string is not in any way related to the empty language

Acceptance

• \(M\) accepts string \(w = w_1w_2\ldots w_n\) if:

\[ \forall w_i \in \Sigma : \exists r_0r_1\ldots r_n : \]

\[ r_0 = q_0 \land \]

\[ r_n \in F \land \]

\[ \forall i : r_i = \delta(r_{i-1},w_i) \]

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• ✓ Kripke Structures
• ✓ Linear Temporal Logic
• ✓ Büchi Deterministic Finite Automata
  • ✓ DFAs
  • Safety & Liveness
• CIA Triad

Safety and Liveness

• The Paper

A formal characterization for safety prop- erties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a prop- erty to be decomposed into a safety property and a liveness property whose conjunction is the original.

Traffic Light

• Büchi traffic light (traffic lights don’t have to stop someday, so not DFAs)

Safety

• “Bad thing won’t happen”
• If a Büchi Automata is a safety property…
  • If the bad things happens, the system is unrecoverable.
  • Therefore, any failures result from “falling off” the diagram.
  • Therefore, all states are accepting states (no failures based on ending).

Safety

• The unsafe thing is “green to red”

Accepting States

• These should, properly, be denoted with double circles (as they accept)

Closure

• The closure of Büchi Automaton given by A ≔ {Q, Σ, δ, q0, F } is cl(A) ≔ {Q, Σ, δ, q0, Q }.

• That is, cl(A) is equivalent to A if the set of accepting states F is expanded to include all of the states of A

• That is, all circles are double circles.

Safety

• A safety property is a property given by a Büchi Automaton A ≔ {Q, Σ, δ, q0, F } such that all traces accepted by A are also accepted by its cl(A) ≔ {Q, Σ, δ, q0, Q }.
• We do not require that Q = F, just that the accepted traces are the same.

Safety

• This means, we can develop safety properties from arrows (edges), or from δ
  • Traffic lights must not allow \(R\) immediately after \(G\)?
  • No problem, make a state “last was \(G\)”
  • Have no defined outgoing edges labeled \(R\)
• Wait…

LTL

• That’s just LTL
  • G X red \(\implies \neg\) green
  • G \(\neg\) green \(\lor\) \(\neg\) X red
• LTL and Büchi automata are equivalent
  • Proof left as an exercise to the student.
  • Possibly the most interest proof of all time.

Liveness

• “Good thing eventually” e.g. F_good_
• If a Büchi Automata is a liveness property…
  • No matter what happens, the system is recoverable.
  • Therefore, any failures result from not reaching accepting states.
  • Therefore, all states should have outgoing edges covering all letters of the trace alphabet.

Liveness

• I’d argue a light must be green eventually.

Liveness

• The closure of Büchi Automaton given by A ≔ {Q, Σ, δ, q0, F } is cl(A) ≔ {Q, Σ, δ, q0, Q }.

• That is, cl(A) is equivalent to A if the set of accepting states F is expanded to include all of the states of A

Liveness

A liveness property is a property given by a Büchi Automaton A ≔ {Q, Σ, δ, q0, F } such that cl(A) ≔ {Q, Σ, δ, q0, Q } accepts all possible traces in Σ^ω.

Liveness

• This means, we can study liveness properties by adding a self-loop with negation of all other outgoing edges to each automaton state.
  • This isn’t great.
• It is more common to add a “trap state” which captures these transitions but does not accept.

Intersection

• We recall set theoretic intersection… \[ \forall e : e \in A \lor e \in B \implies e \in A \cup B \]

• What are these automata accepting again?

Note

A trace property is a set of traces.

Claim

Given a Buchi automaton m, it is not difficult to construct Buchi automata Safe(m) and Live(m) such that Safe(m) specifies a safety property, Live(m) specifies a liveness property, and the property specified by m is the intersection of those specified by Safe(m) and Live(m).

Example

Consider the following Büchi automata over the alphabet of lower case letters:

Example

• Safety means G a ∨ b
  • Safe(m) = {"a", "b", "aa", "ab", "ba", "bb", "aaa", "aab", ... }
• Liveness means GF a
  • Live(m) = {"a", "aa", "ba", "ca", "da", "ea", "fa", "ga", ... }
• The intersection represents elements in both Safe(m) and Live(m)…

Safe()

• We recall the definition of safety.

Safe(m) excludes the “bad thing” for a Buchi automaton, which is attempting an undefined transition, because if such a “bad thing” happens at any point in the trace, the Buchi automaton will not accept that trace.

Safe()

• A core “nicety” of Büchi Automata is that the safety property is the closure.

• Safe(m) = cl(m)

Live()

• We recall the definition of liveness.

Live(m) requires the “good thing” for a Buchi automaton, which is entering an accepting state infinitely often, because we require this “good thing” to happen for trace to be accepted.

Live()

“Consider the following Büchi automata over the alphabet of lower case letters”

Live()

• While safety is mostly about F, the accepting states or the double circles, liveness is mostly about Σ = {a, b, ?}, the alphabet or the possible states of the trace (NOT the states of the automata) that form the labels on arrows.

Live()

• Define liveness relative to Σ.
• There most be no undefined transitions (that would be safety)
• So we require that any letter in Σ has a defined transition at any point in time.

Learn more

• DFAs
• Büchi automaton
• LTL
• Safety & Liveness

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• ✓ Kripke Structures
• ✓ Linear Temporal Logic
• ✓ Automata
• ✓ Safety & Liveness
• CIA Triad

Quoth WUSTL

The CIA Triad—Confidentiality, Integrity, and Availability—is a guiding model in information security. A comprehensive information security strategy includes policies and security controls that minimize threats to these three crucial components.

Confidentiality

Confidentiality refers to protecting information from unauthorized access.

• Quoth Prof. C: That’s RSA, and it is safety.

Integrity

Integrity means data are trustworthy, complete, and have not been accidentally altered or modified by an unauthorized user.

• Quoth Prof. C: That’s SHA, and it is safety.

Availability

Availability means data are accessible when you need them.

• Quoth Prof. C: That’s liveness.

Extended Pillars

• Modern infosec often includes two more:
  • Authenticity
  • Non-repudiation
• No great sources on this, think it’s mostly people selling certs like destcert

Authenticity

Authenticity is the property that an entity is what it claims to be.

• That’s digital signatures, a combination of C and I

Non-repudiation

Non-repudiation is defined as the ability to prove the occurrence of a claimed event or action and its originating entities.

• That’s proof-of-work + authenticity.

Today

• ✓ Threat and Threat Models
• ✓ (Trace) Properties
• ✓ Kripke Structures
• ✓ Linear Temporal Logic
• ✓ Automata
• ✓ Safety & Liveness
• ✓ CIA Triad

Final Thoughts

• We learned this term
  • Pointers/Mem Safety + Recursion
  • Data Structs (List, Stack, Heap, Map, Tree)
  • Modern development (Containers + CI)
  • System programming (C89, Make, .sh)
  • Cryptography (RSA, SHA)
  • Number, Set, Graph, Automata Theory
  • Cybersecurity (Threat Models, CIA+)