RE: Programming languages used for security

["David Crocker" <dcrocker () eschertech com>]

Crispin Cowan wrote:

> >
The above is the art of programming language design. Programs written in
high-level languages are *precisely* specifications that result in the
system generating the program, thereby saving time and eliminating
coding error. You will find exactly those arguments in the preface to
the K&R C book.
<<

Whilst I agree that the distinction between specification and programming
languages is not completely clear cut, there is nevertheless a fundamental
difference between specification and programming.

In a programming language, you tell the computer what you want it to do,
normally by way of sequential statements and loops. You do not tell the computer
what you are trying to achieve. Indeed, current programming languages provide
hardly any means of expressing what you want to achieve; typically, the only
concession they make in this direction is an "assert" statement, which lacks the
expressivity needed (e.g. you can't easily use an assert statement to say that
an array contains the same objects that it did on entry to the current function,
but they are now arranged in ascending order).

In a specification language, you tell the computer what you are trying to
achieve, not how to achieve it. This is typically done by expressing the desired
relationship between the input state and the output state. The state itself is
normally modelled at a higher level of abstraction than in programming (e.g. you
wouldn't refer to a hash table, because that is implementation detail; you would
refer to a set or mapping instead).

The distinction becomes somewhat blurred when you assemble a program from
library classes, because you are relying on those classes to represent some data
without worrying about how they represent it, and calling their methods to
achieve some state changes without worrying about the steps they go through to
achieve it. Unfortunately, in the absence of precise specifications for those
classes, it sometimes happens that what is achieved by calling a method is not
quite what you wanted; or you may sometimes fail to meet the preconditions of
the method, resulting in a crash or exception.

My belief is that a software development language should be capable of
expressing both specification and programming. Most of the time, its users will
write the specifications and let a tool refine them to a program. Where a higher
degree of optimization is needed, the software developer can manually refine
parts of the specification to a program.

It is not difficult to extend such a language to be capable of expressing
expected behaviour as well. This paves the way for tools that attempt to prove
that the specification exhibits the expected behaviour (and that any manual
refinements are correct implementations of the corresponding specification).

In case anyone is wondering what this has to do with security, "expected
behaviour" includes things like "array indices are always in bounds" (i.e. no
buffer overflows no matter what input is provided), and "the browser address bar
always shows the full URL of the current page".

David Crocker
Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com