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

2004-07-12 Thread 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 KR 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

2004-07-12 Thread 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] Education and security -- another perspective (was ACM Queue - Content)

2004-07-12 Thread Fernando Schapachnik
En un mensaje anterior, Blue Boar escribió:
 Fernando Schapachnik wrote:
 I smell a discusion going nowhere. What is the point of teaching a 
 languague?
 Teach them to program in a paradigm (better, in all of them, and give them 
 the
 tools to make educated choices about which is better for each context), and
 choose any language as an *example* of the paradigm.
 
 Ah... but beyond design problems, aren't most security problems 
 language-specific abuses and bugs?  I'm thinking things like I didn't 
 realize it would let me mix signed and unsigned... I didn't realize it 
 would let me right off the end of the buffer... I didn't realize I had 
 to escape or filter certain characters

Same thing happens with concurrency. You need to tell them about shared
variables, mutexes, locking, atomicity, protected sections, etc. When they are
going to undertake a real project in a specific language they need to know how
these are implemented there. I expect them to be able to learn that from the
multiple available resources, once the foundations are learn.

Now s/concurrency/security/. Imagine next year, when language NEW appears
and some people from this list are required to work in it. I suspect most
of them would probably apply their existing knowledge and some searching around
to understand the new thread model, and act acordindgly. Is the same scenario
for students.

Regards.

Fernando.





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

2004-07-12 Thread 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

2004-07-12 Thread 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
 
 




[SC-L] Secure Coding Themes

2004-07-12 Thread Blue Boar
So in all the discussions, I think I'm seeing several main themes:
-Some holes are design or logic errors (possible in any language)
-Some holes are failures to code safely in a given language (language 
specific; possibly addressable by switching to a safer language)
-Some holes are harder to implement in a safer language (library, 
class...)

And I'm sure I've missed a few important ones.
Point is, I think in a number of cases, we mix these concepts in the 
same discussion, and I'm not sure that's always useful.

If we're talking about logic problems... you can always get your boolean 
conditional jump backwards, doesn't matter what language you use.

If we're talking about one flavor of secure coding (coding safely in a 
dangerous language), then that discussion/class neccessarily needs to 
be very language specific.  This problem also extends to things like 
system APIs, libraries, and so on.  I don't know that any significant 
project can get away from that, regardless of the main language used.

If we're talking about secure coding in terms of picking a language that 
should help us not make whole classes of mistakes, then that's a 
different discussion.

		BB


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

2004-07-12 Thread 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