Kevin Wall wrote:


> 2. Do we need programming languages at all? Why not write precise 
> high-level specifications and have the system generate the program, 
> thereby saving time and eliminating coding error? [This is not yet 
> feasible for operating systems, but it is feasible for many 
> applications, including many classes of embedded applications].

Well, I guess I'd argue that this is _somewhat_ irrelevant. If you are proposing
something like Z or VDM, than that in essence becomes your programming language
for all practical purposes. How it's translated to machine code is not what I
was trying to get at. IMO, I think that formal programming languages have their
place, but given that 95% of programmers are weak in formal proofs, they are
likely to be at least as error prone as more conventional programming languages
for all but a select few.

Even when programmers are not weak in formal proofs, they don't have time to do
them. That is why it is essential to have the proof attempts done automatically,
by the computer.

So, if you wish, you can rephrase my original question from "general purpose
programming language" to "general purpose high-level specification method". In
either case, what would you like to see to specifically support writing secure
software? (Obviously, the details will vary at spec methods vs. traditional prog
languages as you are working at different levels, but I think my questions could
be generalized / extended to deal with specifiction languages as well.

OK, I'll take "programming language" to be extended to include specification
languages with code generation facilities. I can't claim to be an expert in
security (I hang out here mostly to learn what the pressing issues are). But I
can see the following language needs for secure programming:

1. Features that help avoid mistakes. Such features are valuable in all
programming domains (not just security) and include things like strong typing,
automatic memory management, few or no automatic type conversions. I regard
portability as important too because applications are often ported between
machines (e.g. many applications are about to be ported/being ported from 32 to
64 bits).

2. Features that help to make the program secure and robust for all inputs (for
example, to prevent buffer overflows). My preference here is for an automated
tool to generate properties of the form "for all possible inputs to this module,
this array index will be in bound at all times" and then generate the proof
automatically (or point out the likely error). Second best is run-time bounds
checking; this will prevent buffer overflow attacks causing security breaches,
but will typically turn such attacks into denial-of-service attacks, unless the
exception handlers are very well written (which is unlikely, because had the
programmer anticipated the attack enough to write a decent exception handler, he
would probably have avoided the bounds breach in the first place).

3. A well-documented library of trusted components for handling
security-specific issues.

4. A mechanism for specifying properties that must be maintained for the system
to be considered secure. I'm thinking of properties like "at all times, the
browser address window will contain the full URL of the current page". Plus
automated proof support to ensure these properties are maintained. If automated
proof support is not provided, run-time checking is a poor second best (poor
because for many security issues, the attack string is so specific that it is
unlikely that it will be found during testing even with a large body of
randomly-generated input messages).

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

Reply via email to