Tag: verification

Categories
vy papers

Specifying digital systems using sequential functions

These papers introduce sequential functions for specifying digital systems  like operating systems and networks.  The mathematical basis comes from Moore machines, Moore machine products, and  primitive recursive functions on finite sequences.  Primitive recursive functions on sequences were described by Rózsa Péter  in the 1950s but their connection with automata was not explored. They provide an alternative to state diagrams and other traditional methods of defining Moore machines, and can concisely define very large scale state machines, interconnected machines, and abstract properties of the machines. Composition of primitive recursive sequential functions corresponds to automata products.  The method is aimed at system designs, not verification of program text and is intended as an aid to system designers so that they can understand properties of their systems before writing code.  The first paper is an introduction to the method and includes a number of examples, one of which is a proof that Paxos is safe.

 State machines for large scale computer software and systems

The second paper shows how to use sequential functions define temporal logic like properties – for example, that something is always true, or must become true “eventually”. The sequential function analogs are more expressive – for example, eventually can be made to depend on different types of events and to work with systems that combine components that change state at different rates and in response to different events.

Specifications like temporal logic but with ordinary mathematics

The third paper gives some historical background on automata theory and argues that the 1970s consensus in Computer Science, that classical automata theory is too limited, was incorrect and ignored, in particular algebraic automata theory and automata products. The paper includes a discussion of  “machine homomorphism” introduced in the 1960s, then modified in  process algebra, and then  eventually forgotten in the process algebra and larger formal methods literature. By the mid 1960s, Moore machines and concurrent products of Moore machines were well understood in the automata theory literature, but for a number of reasons, they were not applied to software specification.

Process algebra and automata theory

Also see Digital Circuits as Moore Machines for models of the real-time behavior of simple digital circuits

 

Unlike most Computer Science research on specification, there is no formal logic or other use of axiomatic methods, no lambda calculus,  no non-determinism, no completed infinities (e.g. infinite sequences of events), not even any category theory needed for sequential functions. Then there is a paper defining modularity mathematically in terms of automata products (improving A mathematical basis for understanding software modularity ). And there is a paper that just presents the theory of sequential functions focused on the mathematics, not the CS applications.

The works are released under the creative commons NC-ND  license   with the added condition that use for training or other purpose in Artificial Intelligence systems is specifically prohibited as violating the prohibition on creating derivative works and/or use for profit. 

Categories
operating systems systems

A claimed validated operating system.

The claim: we have demonstrated the comprehensive formal verification of the seL4 microkernel, with a complete proof chain from precise, formal statements of high-level security and safety properties to the  binary executable code. GD

The L4 base is useful –  we advocated a similar approach with RTLinux which was, um, very similar to L4. It looks like the L4 version here uses the interrupt emulation method at the heart of RTLinux (of course, without any attribution or reference). Just for the record, here’s a much earlier RTLinux based effort.

As for the verification, I am highly skeptical of the claim. Here’s the claimed proof and the research paper.  It’s not at all clear exactly what was validated, but from the paper it looks like the 8000 odd lines of l4 microkernel were shown to provide the functionality described in the Hoare logic specification. No device drivers appear to have been validated.

Categories
Uncategorized

State machines and circuits

The cross coupled latch is one of the greatest inventions of the 20th century

State machine models of timing and circuit design

Categories
software security

Updated Dijkstra vs Perlis (really, DeMillo)

See below.

Categories
academics software security theory

Dijkstra versus Perlis (updated)

Bertrand Russell.
Bertrand Russell.

Dijkstra wrote:

He [Perlis] published a very obnoxious paper arguing against a mathematical approach to programming cite

The paper  by De Millo, Lipton and Perlis  starts as follows:

Many people have argued that computer programming should strive to become more like mathematics. Maybe so, but not in the way they seem to think. The aim of program verification, an attempt to make programming more mathematics-like, is to increase dramatically one’s confidence in the correct functioning of a piece of software, and the device that verifiers use to achieve this goal is a long chain of formal, deductive logic. In mathematics, the aim is to increase one’s confidence in the correctness of a theorem, and it’s true that one of the devices mathematicians could in theory use to achieve this goal is a long chain of formal logic. But in fact they don’t. What they use is a proof, a very different animal. Nor does the proof settle the matter; contrary to what its name suggests, a proof is only one step in the direction of confidence. We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem–and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail.

To me, the problem with Dijkstra is that he was so sharp and such a good writer that he was able to make persuasive cases out of obviously wrong ideas. Dijkstra wanted to be a scientist in the model of theoretical physics, not an engineer. I’m pretty confident that Dijkstra was wrong: programming is engineering – in fact, physics is not as far from engineering as some people would like to believe. I’m not a huge fan of the engineering discipline as it exists in the USA. It has all sorts of negative aspects – including those Dijkstra railed against. But the vision of a programmer as, not a mathematician, but a formal logician flying far above the grubby compromises and trade-offs of mere engineering in a platonic bubble of pure reasoning is wrongheaded.

Dijkstra published some criticism of the Demillo paper at the time and in their response the authors stated something that, as far as I know, remains true

We must begin by refusing to concede that our confidence in a piece of real software has ever been increased by a proof of its correctness

When I was in graduate school (a long time ago), a famous formal methods sctandem_mugholar came for a talk and explained to us that formal methods were needed if we were ever going to develop fault tolerant software. I pointed out that, for example, the Tandem Software worked pretty well in practice. “It cannot”, retorted the famous scholar.

So there.

Here’s Edsger Dijkstra discussing the birth of the use of axiomatics in computer science – the start of “formal methods” research.  What’s striking is the assumed choice between “axiomatic” and “mechanistic” as if there was no other way. In a later note he writes:

And now we are back at our old dilemma. Either we take by definition all properties of the model as relevant, or we specify in one way or another which of its properties are the relevant ones. In the first case we have failed to introduce in the name of “divide et impera” an interface that would allow us to divide and rule and the study of how we could build upon the (only implicitly defined) interface seems bound to deteriorate into a study of the model itself; in the second case we are again close to the axiomatic method….

[…]

Or, to put it in another way: if the traditional automata theory tends to make us insensitive to the role interfaces could and should play in coping with complex designs, should it then (continue to) occupy a central position in computing science curricula?

And I’m struck by the idea  that seems utterly wrong to me, that one either uses the methods of formal logic OR one is stuck without any ability to abstract or underspecify,  And it’s also interesting to see this impoverished view of automata theory that underpins so much of the formal methods literature.

The reason mathematics has advanced so much was not because of the Euclidean axioms-lemma-theorem straitjacket, but in spite of it. Luckily, when we actually discover mathematics, we do it the Babylonian way, empirically and algorithmically. It is only when it is time to present it, that we put on the stifling Greek formal attire.

so says Doron Zeilberger

 

Updated:  with minor format improvements 2/16/2016 and merged with an earlier article 10.2.2016 Erev RH.