Re: [SC-L] Programming languages used for security

[ljknews]

At 10:39 AM -0700 7/14/04, Blue Boar wrote:
>ljknews wrote:
>
>> At 11:38 AM -0700 7/13/04, Blue Boar wrote:
>> 
>>>ljknews wrote:
>>>
The environment with which I am most familiar is VMS, and tradition
is what guides secure interfaces.  Inner mode code _must_ probe any
arguments provided from an outer mode, probe the buffers specified
by descriptors provided, etc.
>>>
>>>What do you do when you're handed a bad pointer?
>> 
>> Return SS$_ACCVIO.
>
>So you put in an error handler that catches access ciolation before you try to use 
>the pointer?  OK, fair enough.  What if the pointer points to memory you own, but not 
>the right kind?

The inner mode code probing ensure that the calling mode has the ability
to read and/or write the memory (according to the semantics of the particular
interface.

The inner mode code does not distinguish between stacks and various heaps,
just that the memory is readable or writable by the calling process in the
mode from which the call is made.

> I have always been under the impression that raw pointers could always cause you 
> problems.  I've assumed that a secure language would have to eliminate that as a 
> type.

As have I.
-- 
Larry Kilgallen

Re: [SC-L] Programming languages used for security

[Blue Boar]

ljknews wrote:
At 11:38 AM -0700 7/13/04, Blue Boar wrote:
ljknews wrote:
The environment with which I am most familiar is VMS, and tradition
is what guides secure interfaces.  Inner mode code _must_ probe any
arguments provided from an outer mode, probe the buffers specified
by descriptors provided, etc.
What do you do when you're handed a bad pointer?

Return SS$_ACCVIO.
So you put in an error handler that catches access ciolation before you 
try to use the pointer?  OK, fair enough.  What if the pointer points to 
memory you own, but not the right kind?  I have always been under the 
impression that raw pointers could always cause you problems.  I've 
assumed that a secure language would have to eliminate that as a type.

BB

Re: [SC-L] Programming languages used for security

[der Mouse]

>> The environment with which I am most familiar is VMS, and tradition
>> is what guides secure interfaces.  Inner mode code _must_ probe any
>> arguments provided from an outer mode, probe the buffers specified
>> by descriptors provided, etc.
> What do you do when you're handed a bad pointer?

I forget whether it's returning an error code analogous to EFAULT or
raising an access violation, but I'm fairly sure it's one of them (at
least under the versions I used).  Either would be reasonable, the
latter arguably more so (just as under Unix, it would arguably be more
sensible to generate a SIGSEGV/SIGBUS rather than returning EFAULT).

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B

Re: [SC-L] Programming languages used for security

[ljknews]

At 11:38 AM -0700 7/13/04, Blue Boar wrote:
>ljknews wrote:
>> The environment with which I am most familiar is VMS, and tradition
>> is what guides secure interfaces.  Inner mode code _must_ probe any
>> arguments provided from an outer mode, probe the buffers specified
>> by descriptors provided, etc.
>
>What do you do when you're handed a bad pointer?

Return SS$_ACCVIO.
-- 
Larry Kilgallen

Re: [SC-L] Programming languages used for security

[Blue Boar]

ljknews wrote:
The environment with which I am most familiar is VMS, and tradition
is what guides secure interfaces.  Inner mode code _must_ probe any
arguments provided from an outer mode, probe the buffers specified
by descriptors provided, etc.
What do you do when you're handed a bad pointer?
BB

Re: [SC-L] Programming languages used for security

[Blue Boar]

der Mouse wrote:
This is not to say that moving up levels is worthless.  But it sounds
to me as though everyone in this discussion is stuck in some kind of
mindset like "if we can just eliminate $CLASS_OF_ERROR, we'll have a
safe and secure programming language".  We won't; we'll just have one
where the unsafe and insecure errors are at a higher level.
Right, that's the game.  We want all the errors to be design and logic 
errors, with no help from the programming language.  (i.e. we don't want 
the programming language to be permitting us to make extra errors.)

The goals should be that 100% of the security problems are design 
errors. :)  Then we can go teach people to design properly...

BB

Re: [SC-L] Programming languages used for security

[der Mouse]

> 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.  [...]

> 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).

I can't help thinking that this is all going to just push the errors up
a level.

When moving from machine code to assembly code, certain errors were
more or less eliminated ("oops, I forgot to update that branch
displacement to account for the extra instruction in between").

When moving from assembly code to C code, certain errors were more or
less eliminated ("oops, I forgot to allocate stack space for that new
local variable").

When moving from C code to, say, Java code, certain errors are more or
less eliminated ("oops, I forgot to update the malloc argument to
account for the extra characters").

But you'll note that in each case, errors remain - errors still occur
at the level of abstraction provided by the language in question.
(Also, as the software responsible for translating the human-written
code into machine-executable code grows in complexity, its bug level
rises correspondingly.)

This is not to say that moving up levels is worthless.  But it sounds
to me as though everyone in this discussion is stuck in some kind of
mindset like "if we can just eliminate $CLASS_OF_ERROR, we'll have a
safe and secure programming language".  We won't; we'll just have one
where the unsafe and insecure errors are at a higher level.

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B

RE: [SC-L] Programming languages used for security

[Nick Lothian]

> 
> Does anyone have pointers to articles on designing API's so 
> that they are
> easy to use securely?
> 

Not specifically related to security, but
http://www.cafeconleche.org/XOM/designprinciples.xhtml#d0e161 is one of the
better things I've seen about designing APIs.

Nick

Re: [SC-L] Programming languages used for security

[ljknews]

At 2:51 PM -0400 7/12/04, Jeff Williams wrote:

>Does anyone have pointers to articles on designing API's so that they are
>easy to use securely?

The environment with which I am most familiar is VMS, and tradition
is what guides secure interfaces.  Inner mode code _must_ probe any
arguments provided from an outer mode, probe the buffers specified
by descriptors provided, etc.

The "easy to use securely" falls out of the general interface methods.
All programming languages on the platform have methods for descriptor
creation, so passing strings of specified length between languages is
not a problem...

...if it is done correctly.  A few releases ago one of the senior
developers at HP approved a call to the operating system that used
C-style strings.  He was shouted down by the user community in a
_very_ loud Usenet discussion and promised that the next release
would provide a standard language-independent method of accessing
the same data.  That was for a mode-of-caller services -- arguably
not really a security problem.

So in addition to safe APIs, it also helps to have critical consumers
who will not stand for unsafe APIs.
-- 
Larry Kilgallen

RE: [SC-L] Programming languages used for security

[David Crocker]

Crispin Cowan wrote:

>>
For years, I have been trying to get formal specification advocates to 
explain the difference between high level programming languages and 
specification languages. From my point of view, "formal specifications" 
can be divided into two categories:

* Those that can be mechanically translated into code, otherwise
  known as "programs"
* Those that cannot be mechanically translated, otherwise known as
  "documentation" :)
<<

Specifications that can readily be mechanically translated to code are often
called "executable specifications".

Specifications that cannot be readily translated to code fall into two groups:

1. They may either be sufficient to completely describe the required behaviour
but expressed in such a way that the machine cannot turn them into a program.
For example, given a sequence s we might specify:

 s'.ranb = s.ranb & s'.isOrdered

Which says that, viewed as an unordered collection, the sequence contains the
same elements as before, but they are now ordered. A sufficiently capable code
generator might realise that a good way to achieve this is to call a method
called "sort"; but to a less capable code generator, this would be
non-executable.

2. They may describe a part of the expected behaviour rather than the complete
behaviour, the intention being that they are expected properties of the complete
specification (or program). For example, if the sequence in the above example is
known to be non-empty, we could specify that the minimum element in the sequence
is the first element (if isOrdered means ascending). These are the sorts of
things that you can do to a very limited extent using assertions in C (and now
Java). I think it is a mistake to regard them as documentation - they are far
more than that.

>>
...
I agree with the other posters: the above could describe a formal 
specification, but could also describe a declarative programming language.
<<

Executable specifications can indeed be related to declarative programming.

>>

However, I think I do see a gap between these extremes. You could have a 
formal specification that can be mechanically transformed into a 
*checker* program that verifies that a solution is correct, but cannot 
actually generate a correct solution. The assert() statements that David 
Crocker mentioned are an incomplete form of this; incomplete because the 
do not *completely* verify the program's behavior to be correct (because 
they are haphazardly placed by hand).

So there's another midpoint in the spectrum: a formal spec that can only 
verify correctness but is complete, effectively is a program for 
non-deterministic machines (cf: NP completeness theory). A spec that is 
incomplete (does not specify all outputs) is more of an approximation.
<<

What you are talking about is "annotated development". Languages/products that
support this include SPARK and ESC/Java. Unfortunately, if you want to use
automated proof, you need to either substantially restrict the language (SPARK)
or accept that the "proofs" are not always sound (ESC/Java). BTW I think both of
those are excellent products in spite of their limitations.

>>
All of which begs the question: are these formal specs that are somehow 
not programs any easier to verify than actual programs? Probably 
somewhat easier (they are necessarily simpler) but some would argue, not 
enough simpler to be worth the bother. E.g. suppose 100,000 lines of 
code reduces to 10,000 lines of formal specification in some logical 
notation. A hard problem, but solvable, is a mechanical proof that the 
10,000 line spec and the 100,000 lines of code actually conform. An 
unsolved problem is "does the 10,000 line spec mean what the human 
*thinks* it means?"
<<

If the code is handwritten in a conventional programming language (excluding the
SPARK subset of Ada) then it is very difficult to get a high success rate using
automated proof. Generating code from specifications (with manual refinement in
a carefully-designed notation where necessary) is not only a faster way to
produce code, it also makes the proofs easier.

As to whether the 10,000 line spec means what the human thinks it means: if the
human is an experienced developer, then it is much more likely to mean what
he/she thinks it means that the 100,000 line program is. Specifications can be
mechanically checked for inconsistency and some forms of incompleteness,
reducing the possibility of error. However, whether the specification means what
the non-technical end-user wants is another matter entirely.

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

RE: [SC-L] Programming languages used for security

[David Crocker]

Peter Amey wrote:

>>
Yes, the "posit and verify" approach.  We adopted this because we think there
are problems with refining specs into code.  One problem is that there can be
(usually will be) more than one valid way of implementing a spec.  For example,
the spec may make the abstract assertion that a list is "ordered".  The
implementation could build an ordered tree structure, write to a buffer that is
periodically quicksorted or even write to a set of temporary files that are
periodically merge sorted.  The design choice may depend on non-functional
requirements such as performance or amount of free memory.  Therefore we don't
see how you can always generate the most appropriate code for the property
"ordered".  
<<

You seem to be assuming that there is only one appropriate solution to the
problem and the system cannot be trusted to find it. In reality, there are often
many appropriate solutions and it matters little which one is chosen. In the
example you give, either of the first two solutions would likely be acceptable,
and I think it would be perverse for a code generator to choose the third (i.e.
an external sort on internally-stored data). But I'm not proposing that you
should have to accept whatever the code generator comes up with: if you don't
like the result, the language should provide a way of expressing (in outline at
least) how you want the "ordered" property to be achieved.

>>
One solution to this is to use very low-levels of specification that avoid the
gap between the abstract concept ordered and the code itself.  This can easily
fall into the trap that the specification language simply becomes code (a
problem with B for example).
<<

You seem to be missing the point that B allows you to specify one abstract
machine that talks about a sequence being "ordered" and then refine it to
another that talks about sorting a list. B does indeed allow you to write
code-like executable specifications; but it also allows you to write
higher-level abstract specifications. I agree that there may be a temptation for
developers to just write the executable version. This is why in PD we have a
semantic distinction between specification and implementation, and you can't
write an implementation without having a specification to attach it to.

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

RE: [SC-L] Programming languages used for security

[David Crocker]

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

Re: [SC-L] Programming languages used for security

[Jeff Williams]

> To get REALLY back to the point, I'd like to comment on Fabien's comment
> that "In my opinion, it's the most important things for a languages,
> something to easily validate user input or to encrypt password are a must
> have."  Fabien is right, but increasingly that's only half the problem.
> There also needs to be something in the libraries for the language to
> securely store data that can't be one-way hashed, as are (inbound)
> passwords.  For example, if I need to store the password my application
> needs to authenticate to a database, or other critical data, it would be
> nice to have that built into the language libraries, instead of having to
> build it myself.  It would certainly reduce the number of programmers who
> build such storage mechanisms themselves, and insecurely at that.

I'm really glad to see this point raised.  I really have very little
interest in the "which language" debate, because most of the software I see
depends so heavily on *libraries*.  The real genius of Java in my opinion is
that they slapped a standard API on top of just about everything (graphics,
databases, networking, phone systems, microplatforms, crypto, and much
more). Some other languages have also been successful here in a somewhat
less standardized way.

But just slapping an API on something is not the same as making it easy to
use securely. Java's JCE is a perfect case in point - they encrypted the API
itself! ;-) To me, it's far more important that the libraries are easy to
use securely than language syntax stuff. So how do we encourage library
writers to write APIs that are easy to use securely?

I'd like to see libraries that force the developer to explicitly do
something special if they want to get around the default secure way of doing
things.  It's not enough to just include a bunch of security features into
the libraries.  I've seen far too many libraries that expose a very powerful
API and make it too easy for a developer to make security mistakes.

Does anyone have pointers to articles on designing API's so that they are
easy to use securely?

--Jeff

Jeff Williams
Aspect Security
http://www.aspectsecurity.com

RE: [SC-L] Programming languages used for security

[Jeremy Epstein]

der Mouse is correct.  I recall a product from the early 80s called "The
Last One".  There was an advertisement for the product on Prof Doug Comer's
door when I was a grad student at Purdue... the claim was that this product
made designing applications so simple that you'd never have to program
again.  I'm sure you're all familiar with this product, since it made your
lives obsolete.

And it would have succeeded, if the Mafia hadn't hushed it up along with
Jimmy Hoffa's death.

One of the buzzwords du jour is "model driven architectures" (MDA); OMG has
a working group on it (http://www.omg.org/mda/).  It's just the latest
iteration in what der Mouse called "very-high-level languages".  It has the
same promises as we've heard by countless iterations of abstractions
faster development, fewer bugs, less need for programmers, etc.  I'm
skeptical.

Getting back to the point at hand, though, I think this discussion is
confusing two related topics: languages that help you build code that
doesn't have security implementation bugs, and languages that help you build
code that doesn't have security design flaws.  [Gary McGraw pushes the
difference between bugs & flaws, and I agree.]  Example: Java helps you
avoid a lot of the common *bugs* (by doing some things automatically like
bounds checking, and providing libraries to do other things correctly like
cryptography], but can't do much to help you avoid misdesigning the
software.  I think we're getting pretty good (relatively speaking) at
building languages for bug-free code, but much less so for flaw-free code.

To me, that's the *real* potential of the very-high-level languages... if
things can be brought up to a point where the design becomes more obvious
(since the implementation becomes somewhat automated), then there's a better
chance of finding the security design problems.

On the other hand, the problem with abstracting too much is that the
security problems can get swept under the rug.

To get REALLY back to the point, I'd like to comment on Fabien's comment
that "In my opinion, it's the most important things for a languages,
something to easily validate user input or to encrypt password are a must
have."  Fabien is right, but increasingly that's only half the problem.
There also needs to be something in the libraries for the language to
securely store data that can't be one-way hashed, as are (inbound)
passwords.  For example, if I need to store the password my application
needs to authenticate to a database, or other critical data, it would be
nice to have that built into the language libraries, instead of having to
build it myself.  It would certainly reduce the number of programmers who
build such storage mechanisms themselves, and insecurely at that.

My $0.02 or equivalent in local currency.

--Jeremy

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of der Mouse
> Sent: Friday, July 09, 2004 4:18 PM
> To: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Programming languages used for security
> 
> 
> > 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?
> 
> Then the "high-level specification" _is_ the programming language,
> albeit a relatively unusual one, with the thing you call "the system"
> being what is normally called the language's compiler.
> 
> Such very-high-level languages are a perennial idea.  As you 
> point out,
> they aren't always appropriate, but when they are they can be helpful.
> But they don't eliminate programming, any more than COBOL (which was
> supposed to make it possible to write programs in plain English and
> thereby eliminate programming as a skill) did.  And they won't
> eliminate coding error.  They'll eliminate certain classes of coding
> error, just as assembly does as compared to machine language, or as C
> or Pascal does as compared to assembly language - but coding errors
> will still occur, just as they do in assembly or C.  They'll just be
> errors at or above the level at which the code is written.
> 
> Or, of course, they'll due to be bugs in the compiler.
> 
> /~\ The ASCII der Mouse
> \ / Ribbon Campaign
>  X  Against HTML [EMAIL PROTECTED]
> / \ Email! 7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B
> 
> 

RE: [SC-L] Programming languages used for security

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of ljknews
> Sent: 12 July 2004 14:24
> To: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Programming languages used for security
> 
> 
> At 3:55 PM -0700 7/10/04, Crispin Cowan wrote:
> 
> > However, I think I do see a gap between these extremes. You 
> could have
> > a formal specification that can be mechanically transformed into a
> > *checker* program that verifies that a solution is correct, 
> but cannot
> > actually generate a correct solution.
> 
> Isn't that pretty much what the SPARK Inspector does ?

Yes, the "posit and verify" approach.  We adopted this because we think there are 
problems with refining specs into code.  One problem is that there can be (usually 
will be) more than one valid way of implementing a spec.  For example, the spec may 
make the abstract assertion that a list is "ordered".  The implementation could build 
an ordered tree structure, write to a buffer that is periodically quicksorted or even 
write to a set of temporary files that are periodically merge sorted.  The design 
choice may depend on non-functional requirements such as performance or amount of free 
memory.  Therefore we don't see how you can always generate the most appropriate code 
for the property "ordered".  

One solution to this is to use very low-levels of specification that avoid the gap 
between the abstract concept ordered and the code itself.  This can easily fall into 
the trap that the specification language simply becomes code (a problem with B for 
example).  Our approach is to embed the property "ordered" as an annotation in the 
code , allow the designer to choose an appropriate solution and then provide 
facilities to show that the implementation preserves the required property.  The SPARK 
Examiner generates the required proof obligations to do this.  There is therefore 
clear blue water between the specification ("what") and the code ("how") but with a 
rigorous way of showing correspondence between them.

Peter


This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

Re: [SC-L] Programming languages used for security

[ljknews]

At 3:55 PM -0700 7/10/04, Crispin Cowan wrote:

> However, I think I do see a gap between these extremes. You could have
> a formal specification that can be mechanically transformed into a
> *checker* program that verifies that a solution is correct, but cannot
> actually generate a correct solution.

Isn't that pretty much what the SPARK Inspector does ?
-- 
Larry Kilgallen

Re: [SC-L] Programming languages used for security

[Crispin Cowan]

David Crocker wrote:
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.
 

For years, I have been trying to get formal specification advocates to 
explain the difference between high level programming languages and 
specification languages. From my point of view, "formal specifications" 
can be divided into two categories:

   * Those that can be mechanically translated into code, otherwise
 known as "programs"
   * Those that cannot be mechanically translated, otherwise known as
 "documentation" :)

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
...
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).
 

I agree with the other posters: the above could describe a formal 
specification, but could also describe a declarative programming language.

However, I think I do see a gap between these extremes. You could have a 
formal specification that can be mechanically transformed into a 
*checker* program that verifies that a solution is correct, but cannot 
actually generate a correct solution. The assert() statements that David 
Crocker mentioned are an incomplete form of this; incomplete because the 
do not *completely* verify the program's behavior to be correct (because 
they are haphazardly placed by hand).

So there's another midpoint in the spectrum: a formal spec that can only 
verify correctness but is complete, effectively is a program for 
non-deterministic machines (cf: NP completeness theory). A spec that is 
incomplete (does not specify all outputs) is more of an approximation.

All of which begs the question: are these formal specs that are somehow 
not programs any easier to verify than actual programs? Probably 
somewhat easier (they are necessarily simpler) but some would argue, not 
enough simpler to be worth the bother. E.g. suppose 100,000 lines of 
code reduces to 10,000 lines of formal specification in some logical 
notation. A hard problem, but solvable, is a mechanical proof that the 
10,000 line spec and the 100,000 lines of code actually conform. An 
unsolved problem is "does the 10,000 line spec mean what the human 
*thinks* it means?"

Crispin
--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix  http://immunix.com

RE: [SC-L] Programming languages used for security

[Wall, Kevin]

David Crocker wrote:

> 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.
[snip]
> 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).

I'm sorry, but I don't quite see how this description sufficiently
delineates between declarative programming languages (such as
SQL, various logic and functional prog langs (Prolog, ML, Haskell,
Miranda, etc.)) from specification languages.

Do you consider them declarative programming languages and specification
languages one in the same? (Note: PLEASE, let's not turn this into a
discussion of language X is / is not a declarative programming
language, especially since the last time I used Prolog was in 1989
and the others I've only read about and/or wrote a few toy
programs. ;-)

My impression always has always been that a declarative programming
language is a high-level language that describes a problem rather
than defining a solution, but that pretty much sounds like your
definition of a specification language.

-kevin wall
---
Kevin W. Wall   Qwest Information Technology, Inc.
[EMAIL PROTECTED]   Phone: 614.215.4788
"The reason you have people breaking into your software all 
over the place is because your software sucks..."
 -- Former whitehouse cybersecurity advisor, Richard Clarke,
at eWeek Security Summit

Re: [SC-L] Programming languages used for security

[der Mouse]

>> Programs written in high-level languages are *precisely*
>> specifications that result in the system generating the program,

> 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.  [...]

This is really just arguing over what words should be used for creating
software using such languages.  You call it "specification" (versus
"programming"), others call it "declarative programming" (versus
"imperative programming").

Personally, I think the latter is the more useful way of looking at it.
Complexity cannot, ultimately, be hidden; build a specification
language powerful enough to build a whole application and it will have
complexity enough that writing useful specifications in it demands the
kind of mental discipline that is usually thought of as programming -
and provides the same kind of capability for expressing error.  (The
errors will be at a higher level, because the language is higher level,
but they will occur if the thing being built is nontrivial.)

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B

Re: [SC-L] Programming languages used for security

[James Walden]

Wall, Kevin wrote:
My vary reason for posing these questions is to see if there is any
type of consensus at all on what mechanisms / features a language
should and should not support WITH RESPECT TO SECURE PROGRAMMING.
For example, you mentioned garbage collection. To that I would add
things like strong static typing, encapsulation that can not be
violated, very restrictive automatic type conversion (if allowed
at all), closed "packages" or libraries or some other programming
unit, elegant syntax and semanatics (oops, said I wouldn't go
there ;-), etc.
In the past few days (actually, all through my career), I've hear a
lot of gripes about what people think is wrong regarding languages,
but little in terms of what they think is valuable.
 

Off the top of my head, I'd like some of the features you mentioned, like
   Garbage collection
   Static typing (with no auto conversions, but with type inferencing)
   Secure encapsulation
I'd also add a rich set of data types, including:
   Numeric types with restrictions as Larry Kilgallen mentioned earlier 
and unlimited precision types
   Strings
   Lists
   Arrays (bounds-checked)
   Associative arrays (aka hashes)
   Unions (as in ocaml, not C, which will also provide enumerated and 
boolean types)
   Functions (first-class functions)
   XML (like Xen)

I also want a taint checking feature like perl's, as a general purpose 
language has to communicate with external programs which don't share its 
data types, like web servers sending CGI parameter strings or databases 
receiving SQL query strings.

As for syntax, I want to be able to use functional, imperative, or 
object-oriented techniques as best fit my problem domain.

--
James Walden, Ph.D.
Visiting Assistant Professor of EECS
The University of Toledo @ LCCC
http://www.eecs.utoledo.edu/~jwalden/
[EMAIL PROTECTED]

RE: [SC-L] Programming languages used for security

[David Crocker]

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

Re: [SC-L] Programming languages used for security

[Dana Epp]

My what a week of interesting discussions. Lets end this week on a good 
and light hearted note.

Admit it. We all know the most secure programming language is Logo anyways.
It's hip to be 'rep 4 [ fwd 50 rt 90]'
Laugh. Or the world laughs at you. Have a good weekend guys.
Crispin Cowan wrote:
David Crocker wrote:
1. Is it appropriate to look for a single "general purpose" programming
language? Consider the following application areas:
a) Application packages
b) Operating systems, device drivers, network protocol stacks etc.
c) Real-time embedded software
The features you need for these applications are not the same. For 
example,
garbage collection is very helpful for (a) but is not acceptable in 
(b) and (c).
For (b) you may need to use some low-level tricks which you will not 
need for
(a) and probably not for (c).
 

I agree completely that one language does not fit all. But that does not 
completely obviate the question, just requires some scoping.

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].
 

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.

Crispin

--
Regards,
Dana Epp
[Blog: http://silverstr.ufies.org/blog/]

RE: [SC-L] Programming languages used for security

[Wall, Kevin]

David Crocker wrote...

> I think there are two other questions that should be asked before
> trying to answer this:
> 
> 1. Is it appropriate to look for a single "general purpose" programming
> language? Consider the following application areas:
> 
> a) Application packages
> b) Operating systems, device drivers, network protocol stacks etc.
> c) Real-time embedded software
> 
> The features you need for these applications are not the same. For
> example, garbage collection is very helpful for (a) but is not
> acceptable in (b) and (c).  For (b) you may need to use some
> low-level tricks which you will not need for (a) and probably not
> for (c).

I did not mean to imply that a *SINGLE* general purpose programming
language be the optimal, end-all, be-all solution for all software
problems. Rather, I was trying to understand what would we, as security
professionals, find useful in a programming language in terms of specific
feature sets, etc. (At this point, I don't even want to particularly
discuss syntax and semantics, although I would argue that these things
do have an impact on secure coding as well.)

The very reason that I stated "a GENERAL PURPOSE programming language"
rather than just "a programming language" is I didn't want the
discussion to digress into fine grained application areas such as
"for web applications, you need features F1 and F2, but for
programming firewalls, you want features F1' and F2'", etc.
For any given application area, I'm of the opinion that you can
design an application specific prog language that will be better
suited and likely offer more security than you can in the general
case. However, this is usually just not practical, which is why we
have other mechanisms to extend the basic functionality of programming
languages (usually application specific libraries). (Of course,
sometimes the language itself goes beyond that; for example Prolog
offers its "Declarative Clause Grammar" form which is great for parsing.
And Forth can be used or abused almost ad infinitum.)

My vary reason for posing these questions is to see if there is any
type of consensus at all on what mechanisms / features a language
should and should not support WITH RESPECT TO SECURE PROGRAMMING.
For example, you mentioned garbage collection. To that I would add
things like strong static typing, encapsulation that can not be
violated, very restrictive automatic type conversion (if allowed
at all), closed "packages" or libraries or some other programming
unit, elegant syntax and semanatics (oops, said I wouldn't go
there ;-), etc.

In the past few days (actually, all through my career), I've hear a
lot of gripes about what people think is wrong regarding languages,
but little in terms of what they think is valuable.

> 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.  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.

-kevin wall

> David Crocker, Escher Technologies Ltd.
> Consultancy, contracting and tools for dependable software development
> www.eschertech.com
> 
> 
> Kevin Wall wrote:
> 
> >>
>If a GENERAL PURPOSE programming language were designed by
>scratch by someone who was both a security expert and
>programming language expert, what would this language (and
>it's environment) look like?
> 
>More specifically,
> 
>   + What set of features MUST such a language support (e.g.,
> strong static typing, etc.)?
>   + Perhaps just as importantly, what set of features should
> the language omit (e.g., pointer arithmetic, etc.)?
>   + What functionality should the accompanying libraries support
> (e.g., encryption, access control, etc.)?
>   + What would be the optimal paradigm (from a theoretical, rather
> than pragmatic perspective) that such a langua

Re: [SC-L] Programming languages used for security

[der Mouse]

> 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?

Then the "high-level specification" _is_ the programming language,
albeit a relatively unusual one, with the thing you call "the system"
being what is normally called the language's compiler.

Such very-high-level languages are a perennial idea.  As you point out,
they aren't always appropriate, but when they are they can be helpful.
But they don't eliminate programming, any more than COBOL (which was
supposed to make it possible to write programs in plain English and
thereby eliminate programming as a skill) did.  And they won't
eliminate coding error.  They'll eliminate certain classes of coding
error, just as assembly does as compared to machine language, or as C
or Pascal does as compared to assembly language - but coding errors
will still occur, just as they do in assembly or C.  They'll just be
errors at or above the level at which the code is written.

Or, of course, they'll due to be bugs in the compiler.

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B

Re: [SC-L] Programming languages used for security

[Crispin Cowan]

Dana Epp wrote:
My what a week of interesting discussions. Lets end this week on a 
good and light hearted note.
Insert various analogies between programming languages and automobiles 
here :)

   * $MY_FAVORITE_LANGUAGE is like a $REALLY_COOL_CAR, while
 $YOUR_FAVORITE_LANGUAGE is like a Yugo.
   * $C_OR_ASSEMBLER_ITS_REALLY_THE_SAME_THING is like a thermonuclear
 missile, in that it is fast and powerful, but if you are not
 careful, you can give yourself an ouchie :)
Crispin
--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix  http://immunix.com

Re: [SC-L] Programming languages used for security

[Crispin Cowan]

David Crocker wrote:
1. Is it appropriate to look for a single "general purpose" programming
language? Consider the following application areas:
a) Application packages
b) Operating systems, device drivers, network protocol stacks etc.
c) Real-time embedded software
The features you need for these applications are not the same. For example,
garbage collection is very helpful for (a) but is not acceptable in (b) and (c).
For (b) you may need to use some low-level tricks which you will not need for
(a) and probably not for (c).
 

I agree completely that one language does not fit all. But that does not 
completely obviate the question, just requires some scoping.

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].
 

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.

Crispin
--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix  http://immunix.com

RE: [SC-L] Programming languages used for security

[David Crocker]

I think there are two other questions that should be asked before trying to
answer this:

1. Is it appropriate to look for a single "general purpose" programming
language? Consider the following application areas:

a) Application packages
b) Operating systems, device drivers, network protocol stacks etc.
c) Real-time embedded software

The features you need for these applications are not the same. For example,
garbage collection is very helpful for (a) but is not acceptable in (b) and (c).
For (b) you may need to use some low-level tricks which you will not need for
(a) and probably not for (c).

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].

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


Kevin Wall wrote:

>>
   If a GENERAL PURPOSE programming language were designed by
   scratch by someone who was both a security expert and
   programming language expert, what would this language (and
   it's environment) look like?

   More specifically,

  + What set of features MUST such a language support (e.g.,
strong static typing, etc.)?
  + Perhaps just as importantly, what set of features should
the language omit (e.g., pointer arithmetic, etc.)?
  + What functionality should the accompanying libraries support
(e.g., encryption, access control, etc.)?
  + What would be the optimal paradigm (from a theoretical, rather
than pragmatic perspective) that such a language would fit into
(e.g., object-oriented, functional, imperative, logic programming,
etc.)? [Note: I mention "theoretical, rather than pragmatic" so
that such a language would be unduly influenced by the fact that
presently developers familiar with OO and imperative styles vastly
out number all the others, with functional coming up a distant
3rd.]
  + (Related to the previous item) Would such a language be compiled
or interpreted or something in between.

Also, if anyone chooses to discuss these issues, let's leave things like
portability and performance out of the equation UNLESS you feel these
things directly have an impact on secure coding. I think that we can
all agree that we'd desire a portable and fast-executing language
(although perhaps a slow-executing language would be more secure in
that it might slow down the propagation of malware ;-).
<<

Re: [SC-L] Programming languages used for security

[Crispin Cowan]

ljknews wrote:
Such typing should include specification by the programmer of the range
of values allowed in variables: -32767 to +32767, 0 to 100, 1 to 100,
Characters a-z only, characters A-Z only, -10.863 to +4.368, etc.
The language should also support exact specification of arithmetic
operations to be performed for various types (overflow semantics,
precision, decimal vs. binary arithmetic, etc.).  This is important
to ensure the desired behavior is obtained when one changes to a
new compiler/interpreter, if only to have a program rejected as
requiring behavior not supported on the new compiler or operating
system.
 

Check out the Hermes programming language 
, 
which not only does such checks, but in many cases can do the checks 
statically, and refuse to compile unsafe programs. This mechanism is 
called typestate checking 
., 
which IMHO is one of the most interesting extensions of static type 
checking for both safety and performance.

The bad news is that Hermes, while it has many great safety features, is 
another dead programming language. That's the problem with programming 
language design: there are LOTS of great programming languages out 
there, and approximately none of them have the critical mass of 
compilers, tools, and (most important) programmers to make them viable 
for most projects.

The good news is that Hermes is among the sources that Java looted; some 
of the typestate checking features ended up in the Java bytecode checker.

Crispin
--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix  http://immunix.com

Re: [SC-L] Programming languages used for security

[Fabien]

Hello,

I'm not a secure coding expert, so my point of view is more from a
developper view.

>   + What functionality should the accompanying libraries support
> (e.g., encryption, access control, etc.)?

In my opinion, it's the most important things for a languages, something
to easily validate user input or to encrypt password are a must have.

And the other good thing with a good base library is that the user don't
need to re-develop his own one. And it's easier to extend, to maintain
and to import the security of a main librairy instead of a lot of 3rd
parties library.

-- 
Fabien, sorry for his english.

Re: [SC-L] Programming languages used for security

[ljknews]

At 8:49 AM -0500 7/9/04, Wall, Kevin wrote:

>   If a GENERAL PURPOSE programming language were designed by
>   scratch by someone who was both a security expert and
>   programming language expert, what would this language (and
>   it's environment) look like?
>
>   More specifically,
>
>  + What set of features MUST such a language support (e.g.,
>strong static typing, etc.)?

Such typing should include specification by the programmer of the range
of values allowed in variables: -32767 to +32767, 0 to 100, 1 to 100,
Characters a-z only, characters A-Z only, -10.863 to +4.368, etc.

The language should also support exact specification of arithmetic
operations to be performed for various types (overflow semantics,
precision, decimal vs. binary arithmetic, etc.).  This is important
to ensure the desired behavior is obtained when one changes to a
new compiler/interpreter, if only to have a program rejected as
requiring behavior not supported on the new compiler or operating
system.

>  + Perhaps just as importantly, what set of features should
>the language omit (e.g., pointer arithmetic, etc.)?
>  + What functionality should the accompanying libraries support
>(e.g., encryption, access control, etc.)?
>  + What would be the optimal paradigm (from a theoretical, rather
>than pragmatic perspective) that such a language would fit into
>(e.g., object-oriented, functional, imperative, logic programming,
>etc.)? [Note: I mention "theoretical, rather than pragmatic" so
>that such a language would be unduly influenced by the fact that
>presently developers familiar with OO and imperative styles vastly
>out number all the others, with functional coming up a distant
>3rd.]
>  + (Related to the previous item) Would such a language be compiled
>or interpreted or something in between.

-- 
Larry Kilgallen