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 www.eschertech.com
