nondeterministic . net

Day 2 of the Semantics and its Applications Workshop, December 20, at Tel Aviv University.

Quantifying Interference

Avoiding Determinization

Modeling Concurrency without Global States

Lunch

Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation

Semantics-Directed Abstraction and Refinement

Semantic Minimizations for Temporal Logics

On the Construction of Fine Automata for Safety Properties

A Semantics for Procedure Local Heaps and its Abstractions

You have no idea the witty gems you’re missing out on if you don’t go over these with a fine-toothed comb.

The math shorthand for directed acyclic graph is DAG. And the Hebrew word for fish is "dag." So when someone asks "is that a DAG or a tree," it really sounds much more like "is that a fish or a tree?"

Which is funny when you’ve been sitting in the same chair for two days with not many fish or trees to be seen.

Quantifying Interference

Pasquale Malacaria, Department of Computer Science, Queen Mary University of London

Motivation: there is no such thing as a secure system

Perfect secrecy: I’d tell you, but then I’d have to kill you

Password checks release information

e.g. every attempted password removes one from set of possibilities

Guess correctly and learn log(search space size) bits

Incorrect and learn log(size) - log(size-1) bits

Eve from 6.095 is totally getting this

Can find sum times probabilities

Definition of Shannon entropy:

The entropy measures the interference between a secret variable and the outcome of a program: I(H,O | L)

Combines probability of an attack with damage it would cause

History: Dennings, Millen, McLean, Gray

Relating information theory and interference

Given a probability distribution on inputs, program variables are random variables

Three interesting variables L, H, O (low and high inputs, output), where O=f(L,H) for deterministic programs

Non-interference: the denotation of a deterministic program is a function constant on the H parameter, i.e. f(h,l)=f(h’,l)

Quantify interference as H(O | L) = “uncertainty in O given knowledge of L”

Proposition: H(O | L) = 0 iff P is non-interfering

H(O | L) = n > 0 measures how easy it is to guess H knowing O, L

Independence vs non-interference

Mutual information I(X,Y)=H(X)-H(Y) = measure of independence

So I(H;O) = 0 iff non-interference? No; example: O = L xor H

I(H;O) ignores the context (L)

Define interference as I(H; O | L) = H(H) - H(H | L, O)

For deterministic programs, I(H; O | L) = H(O | L)

A quantitative static analysis of interference

Measuring information flow in a simple imperative language

Assignment, sequence, loops, conditionals

Only analyzing language constructs (not timing, overflow)

Assume program termination

Analysis produces upper/lower bounds on entropy an attacker can gather about confidential input knowing the public

Trivial examples

h=h; l=l+1: attacker gets 0 bits

h=l; gets 0 bits

l=h; gets k bits for k bit h

Analysis overview

x=e: direct flow: special cases of e can be treated (e.g. l=h mod 2), need taxonomy

while e do c: if there is a bound on the iterations, consider as nested conditions; otherwise, need a rate of leakage analysis

if e then c else c’: indirect flow, subtle leakage

Example: compare high against public variable, modify low

Conditionals: if e then c else c’

Measuring leakage from expression e

Reasonable bounds when e is an equality test that is usually false (difference in entropy is large)

Combine this with leakage from c, c’

H(IF) = the amount of information about a (generic k-bits) program variable x that an attacker can gain by running the IF command

Trick is taking upper bound k on the true branch (thus )

But don’t know , , ,

However, we have bounds on H(c’) (induction hypothesis) which turns out to be enough for

Theorem 16.3.2 in Cover-Thomas

Study of H(e) using upper bound and is enough

Fancy graph goes here

Avoiding Determinization

Orna Kupferman, School of Computer Science and Engineering, Hebrew University

Deterministic machine: single run on every input, accept if it accepts

Nondeterministic: multiple runs, accept if one accepts

Risk is for free

The presenter is trying to make her presentation interesting — what a bizarre concept!

NFW (nondeterministic finite word automata) are exponentially more succinct than DFW

NFW: O(n) states

DFW: states

Sometimes nondeterminism causes no problems

Nonemptyness check

Always have to check reachability, NLOGSPACE, linear time

Membership checking, projection, etc.

Sometimes nondeterminism is problematic

Complementation L(A’)=comp(L(A))

DFW: dualize acceptance condition

NFW: need all runs rejecting, as opposed to exists rejecting run

Running A on a tree ()

Given an NFW A, want that accepts all trees all of whose paths are accepted by A

Simple construction forces guesses to be about all paths of left and right subtrees

Applications: deciting CTL*, -calculus, solving games with -regular goals, LTL realizability and synthesis

Usual solution: determinize

Problem: exponential blow-up

Problem (for automata on infinite words): very complicated

Automata on infinite words

Büchi acceptance: visit infinitely often

There is no DBW for

Safra’s construction

First optimal construction, beautiful, very complicated, Berkeley tried to implement it in the 90’s but gave up

Motivation

Model checking: have tools

Synthesis: no tools

Universality

Machine has multiple runs on every input

Accepts when all runs accept

Example: old NFW for (0+1)* is now UFW for (0+10)*

Sufficiently strong to serve as intermediate automata in many applications in which deterministic automata are traditionally used as intermediates

Complementation

Finite words

Curently: NFW to DFW, dualize to

Now: NFW dualize to , to

Where dualize means both branching mode and accepting condition

Second step uses subset construction

Infinite words

Currently: from NBW, determinize to DRW, dualize, then translate to NBW

Now: take NBW to complementary UCW (co-Büchi acceptance: visit finitely often), then translate to NBW

Example

Pretty pictures

If you like pictures of circles and arrows with numbers as chiaroscuro

-calculus satisfiability

Easy to construct APT for -calculus that accepts all trees satisfying

Old: need to convert APT to NPT, and check its emptyness

New: convert APT to UCT (emptyness equivalent UCT, similar to NPWNBW), and check its emptyness (use conversion to NBT)

Synthesis

Given LTL formula over input I and output O, construct a finite-state strategy that generates only computations that satisfy

Idea: open system, for each input, generate output that is function of all inputs seen so far

Is realizable?

Old

Construct DRW (Rabin) accepting computations satisfying

Run on the I-exhaustive tree

Check emptyness of the NRT

New

Construct NBW that accepts computations satisfying

Run the dual UCW on the I-exhaustive tree

Check emptyness of the UCT

Magic: UCW to NBW and UCT to NBT

Based on analysis of accepting runs of co-Büchi automata

Summary: Universality replaces Safra’s construction with much simpler procedures

Modeling Concurrency without Global States

(with Traskian structures instead)

Uri Abraham, Ben Gurion University

Accepted paradigm of concurrency

A global state is an instantaneous description of the system; some states are initial states

A step, or action, can atomically change a global state into another

A history is a sequence of global states, beginning with an initial state and such that every state and is successor in the history for a step; a system is modeled by the set of all possible histories, this is the interleaving semantics

A correctness condition is some temporal logic sentence ; if holds in every history, then the system satisfies

Alternative paradigm: formal behavioral reasoning

Events (which may be extended in time) are the main objects, not global states

System executions instead of histories; these are special Tarskian structures

Relations and functions are defined over the events; vs histories, which do not contain functions or relations over step occurrences

Both low and high level events (operation executions) are events

Interested in understanding, in finding a natural framework for proofs

Claim: behavioral reasoning can be made completely formal

Example: local clocks protocol

Idea: write time to register, wait until other process have later time, then run critical section

Boardwork!

Assumptions

Clock is monotonic: non-overlapping clock reads return increasing values

Registers are safe; register R is safe if:

Write events are serially ordered; there exists an initial write that proceeds all reads

For every read, either the read overlaps with a write, or the value read is the value written by the latest preceding write

System executions

Signatures

Three sorts: Event, Atemporal, Moment (subsort of Atemporal)

Binary relation temporal precedence < on Event

Binary relation < on Moment

Unary predicate terminating on Event

Function Begin and End from Event into Moment: event e in closed interval

A system execution is an interpretation M of a system execution signature s.t. …

Speaker is under some fire for saying things that make sense instead of mathematical garblygook

Example

Safe register signature

Sorts as above

Predicates as above, plus unary Writer and Reader on Event

Functions as above, plus Val from Event to Data

Safe register direct specification

Reader and Writer events are terminating

Events in Writer are serially ordered

The first Writer precedes all Reader events

For Reader r s.t. for every Writer w we have w < r or r < w, if w is the rightmost Writer s.t. w < r, then Val(r) = Val(w)

Safe register specification with return function

Return function from Event to Event

Reader and Writer events are terminating

Events in Writer are serially ordered

The first Writer precedes all Reader events

For Reader r, is a Writer s.t. , , and

This definition is equivalent in the sense that for any structure satisfying the first, we can define as needed, and the reverse

Questions

Formal proofs will always be hard to read; goal is finding proofs where relying on your intuition to help you through a proof is OK and helpful

You can tell people actually understood this lecture because they have technical bones to pick

Lunch

Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation

Orna Grumberg, Computer Science Department, Technion

with Rachel Tzoref

who is a masters student

and did all the animations

Symbol Trajectory Evaluation

Hardware model checking technique handling larger hardware designs within a restricted specification language (widely used)

Given circuit M, specification (antecedent and consequent in TEL)

Currently: construct abstract model M for A, , check if

Pass:

Fail: gives counterexample

Undecided: refinement needed (manually on A, thus on

New

Automatic refinement of A, s.t.

Define and detect vacuity in STE

Pass is vacuous, or counterexample is spurious

Define 3-valued semantics for logic TEL corresponding to 3 STE results

Modeling a circuit

Graph where nodes are inputs, gates, and latches

Input: nondeterministic value

Gate: value from current time

Latch: value from previous time

Refer to nodes at different times

Look at unwinding of the circuit for k times, k determined by

Example circuit, with animations

Describe node values with 4-value lattice: 0, 1, X,

X for unknown, used to obtain abstraction

for over-constrained, used to denote contradiction between circuit behavior and requirements of antecedent A

Meet operation is the greatest lower bound of a and b

Join

Quarternary operations: rules for X and

Symbolic execution of a circuit

Propagate variables through circuit

Obtain a series of abstract (contains X) symbolic states

Trajectory Evaluation Logic (TEL)

(n is p): node has symbolic value p

: f is a formula

: conjunction

N(f): next operator

3-valued semantics of TEL formulas

Interpreted over symbolic sequence over V, and assignment

= true, false, or unknown

: abstraction of M derived by A, the weakest symbolic trajectory

is a symbolic sequence of M that satisfies A

For every symbolic sequence of M,

Known: for every circuit M and TEL formula f, we have

This is the abstraction of M containing just enough information to know about A

STE checks

Compute

Check that this also satisfies C

Refinement

Choose for refinement a set of inputs at specific times

For each , is a fresh variable not in V

Refined antecedent is

Goal: add a small number of constraints, keeping relatively small while eliminating as many undecided results as possible

Eliminating some may still reveal fail; need all eliminated for pass

Strategy: choose one refinement goal (root, tt) which is undecided with dependency on minimal number of inputs

Naïve solution: (n,t) for (root, tt)

Add semantic requirement: only change roots where everything on path from root to goal is X

Vacuity detection

Example (animated, of course) of spurious counterexample

Refinement yields node with bottom, so counterexample is not a real run

Future: automatic refinement for Generalized STE where specification language is as expressive as -regular languages

Questions:

You said GSTE more difficult… but is it still possible? You can still define the little black dot and everything?

Semantics-Directed Abstraction and Refinement

Dan Ghica, School of Computer Science, University of Birmingham

with A. Dimovski, R. Lazic, and C. Hermida

Presenter is using Keynote

Model checking: does a system satisfy a property?

Conversion from software to model: examine state explored by program

Game semantics & MC

Example: int p(void c(int d)) { int x = 1; c(2); return x; }

Should always return 1

How to represent non-local procedure calls?

Example: imperative call-by-name language

Game semantics is not looking at state; rather at function calls and returns

For function f, model describes all ways f might (or not) evaluate arguments

Models compose naturally similar to automata products

Verifying abstract data types (ADTs)

Example: stack, gives a shortest trace to overflow for “pop returns last push”

Example: sorting

Cell phone

Abstract interpretation

Diagram where crossing edge has a little EE-style hump

Somebody is using OmniGraffle

Abstract components to reduce states and edges

Introduces false traces, but that’s the price you pay

For leading such a life of crime

Example

Referring to “if (x=x+1) then abort:” if you’re a little bit, you know, not blind, you can see this is not a real error

Abstraction reduces infinite model to simple finite model where some transitions have 0,1 value; this is the imprecision, see note above about life of crime

An abstraction:

With nondeterminism, takes us from language with infinite integers to finite models

Same cell phone

Proof of soundness

Need to show soundness w.r.t. game semantics (i.e., introduces false errors, but doesn’t hide real errors)

Right Kan extension: some categorical notation having to do with approximation

Most precise approximate that goes from abstract result to real result produced by original program

Existence

p goes

Abstract C and C’ with A and A’ by and

Take , which goes

Square diagram shown

Multiabstractions: use identity to do composition, which looses information, but is unavoidable

Abstraction of strategies

Return to example

Finding spurious examples: need to do composition without hiding, to reveal intermediate results, from there find over-approximations and refine

Implementation: done only in a particular play, to retain the advantage of game semantics that internal actions are hidden

Ranking to determine where to refine

Implementation: we have one

GALOP Workshop at FLOC’06

Get it? Get it?

Symbolic vs. symbolic

Orna: academic freedom is the source of all evil

Semantic Minimizations for Temporal Logics

Michael Huth, Department of Computing, Imperial College London

with Patrice Godefroid

The ‘d’ at the end is silent

Propositional Logic

Applications of abstraction: state, behavior, interface, topology, shape analysis, space-time

Need for “may” and “must” information, c.p. yesterday’s aspects talk

Models

1/2 = X

Refinement: if M gives a definite answer, refinement M’ must agree

M is 2-valued if

Thorough semantics: iff all 2-valued refinements satisfy in standard semantics

Galois adjunction

3-valued model M determines a set of 2-valued models through refinement

Given such a set, it determines a 3-valued model through “independent attribute analysis”

If you abstract and then concretize, you get at least what you started with

Abstraction of concretization recovers original

Thorough semantics as validity problem

Each M has a formula in proposition with

captures “being a refinement of M;” records all obligations refinements have to meet, and implication on RHS captures “all refinements of M satisfy “

Under-approximating thorough semantics

Seek efficient judgement that under-approximates thorough satisfaction

Define assuming negation normal form

Captures soundness:

Semantic minimization

Seen: reduce to validity check

Can we reduce to model check?

Want: for each , is there a in the same logic s.t.

Call any such a semantic minimization

Known: any of propositional logic has a semantic minimization in propositional logic

Self-minimizing patterns

Computing is coNP-hard

Can we state patterns where is short, or where you can use for (called pessimistically self-minimizing)

Examples: all monotone (no atoms have mixed polarity), if-and-only-if

is not pessimistically self-minimizing, even though is

Temporal Logic

For which temporal logics do we have semantic minimizations?

What proof constructs are used?

Complexity? Patterns?

Partial Kripke structures: 3-value models for propositional logic “extended over time”

Semantics extended over time

“I apologize, many of you may be seeing a one there on the slide, that’s a zero”

Example: calling unknown function, obtain model using predicate abstraction

Refinement

Thorough semantics

Kripke structures are those partial Kripke structures where label never has 1/2

is Kripke structures that refine M

iff for all , N satisfies in standard semantics

is no longer a single model

Galois adjunction (not an insertion) between compact sets of Kripke structures and bounded Scott-closed sets of partial Kripke structures in a fully abstract domain model for refinement

Compositional semantics for modal -calculus

Convert to negation normal form, that hides 3-valuedness

Thorough check reduces to validity check (for finite state M)

Self-minimization for temporal logics

Deciding pessimistic self-minimization reduces to language inclusion check of alternating parity tree automata, EXPTIME-hard

Identify patterns of self-minimization by “efficient grammar”

Define grammar for ps and os (optimistic self-min)

Interesting dependencies on temporal operators

Reducing a validity check to a model check, but doing it uniformly

Semantic minimizations for propositional logic (optimistic)

Consequence: in ALOGTIME

Semantic minimizations for modal -calculus

Semantic minimizations for CTL and CTL*

For each instance of MONOTONE_CIRCUIT_VALUE, we have a partial Kripke structure

Existence of semantic minimizations for CTL in CTL* would imply NLOGSPACE = PTIME

In fact, can show a counterexample, so they don’t

On the Construction of Fine Automata for Safety Properties

Robby Lampert, School of Computer Science and Engineering, Hebrew University

Is ?

System: labeled state transition graph

Path: word over

Specification: temporal logic formula

Or, an automaton on infinite words, with Büchi acceptance condition

, matching lower bound

Checking containment using emptyness check on intersection with complement

Complementation might involve exponential blowup if is an automaton

For in LTL, construct

Eventually arrive to emptyness of Büchi automata

Is empty?

State explosion problem

Solution: symbolic algorithm, work with operators on sets of states, quadratic using nested fixed points

Safety properties

A language L is a safety language if for every word not in L, there is a prefix such that when we concatenate any word onto the prefix, the result is not in L