Raúl López-Rueda

Why narrowing

Narrowing lets a verifier reason about all possible inputs at once, instead of checking them one by one. This page explains the idea, why it helps to verify systems, and where my research fits.

In short

One symbolic state can stand for infinitely many concrete states.

Many systems have infinitely many possible states: counters with no upper bound, unbounded queues of messages, an arbitrary number of processes. Testing, or listing states one by one, can only ever cover a small part of them.

Narrowing explores how a system behaves starting from states that contain variables. Each of those states describes a whole family of concrete states, so a single run of the analysis covers all of them. When the symbolic search can be made finite, it establishes a property for every state in the family. When it cannot, it is still useful: it can find counterexamples, or hand the remaining work to a theorem prover.

Rewriting first

In rewriting logic, the state of a system is a term and each transition is a rule that rewrites one pattern into another. Languages such as Maude make this executable: you describe a concurrent or distributed system with rules, then run it, search its reachable states, or model check it.

Rewriting starts from a concrete term and applies rules until none applies. The example below adds natural numbers, written with 0 and a successor function s. It is the smallest example that still shows the difference between the two techniques.

What narrowing adds to rewriting

Rules rewrite a concrete term, one step at a time, until none applies.

  1. rl 0 + N => N .
  2. rl s(M) + N => s(M + N) .

0 is zero, s(n) is the successor of n, and M, N and X are variables.

s(s(0)) + s(0)
=>s(s(0) + s(0))rule 2
=>s(s(0 + s(0)))rule 2
=>s(s(s(0)))rule 1

No rule applies any more. The result is s(s(s(0))), that is, 2 + 1 = 3.

What narrowing adds

Rewriting needs a concrete starting point. If part of the input is unknown, say the X in X + s(0), no rule can be matched against X and rewriting is stuck.

Narrowing replaces matching with unification. It looks for the substitutions that make a rule applicable and applies the rule under each of them. In the example, X is either 0 or the successor of something, so the step splits into two cases. Together the cases cover every natural number, and each one keeps going on its own.

That is the whole idea. Instead of running the system on one input, you run it on a pattern, and the analysis branches only where the rules force it to.

For verification

Infinite-state systems

A symbolic state with variables describes infinitely many concrete states, so a finite analysis can say something about all of them.

Reachability from a set of states

Instead of asking whether one given state can reach a bad state, you can ask the question for a whole family of states at once. Narrowing is a complete method for this: if a target can be reached from some instance of the starting pattern, narrowing can find it.

Protocol analysis

The messages an attacker may send to a security protocol are not bounded in advance. Symbolic analysis based on narrowing, as in tools such as Maude-NPA, handles that unboundedness without enumerating the messages.

The catch

A symbolic search can still run forever. In the example above, the second branch keeps splitting without end. Making the search finite is where much of the research lies. Three of the main ideas:

  • Folding. A new symbolic state is dropped when one already explored covers it, because it can only lead to behaviours that were already seen.
  • Constraints. Symbolic states can carry constraints that an SMT solver checks, so branches that no concrete state can follow are pruned.
  • Irreducibility. In canonical narrowing, variables are restricted to values that are already fully simplified, which avoids repeating the same work in a different form.

In my research

Further reading