Re: [SC-L] Conditional Compile statements-- coding standards, and code review

2009-02-22 Thread David Crocker
When my organization develops code in C++, we generally ban use of #ifdef and 
#if defined(X), but we otherwise allow use
of #if. The reason is that if you mis-spell the identifier that follows #ifdef, 
the compiler can't warn you. For
example, if you write

 #ifdef FRDE
 ...
 #endif

when you meant #ifdef FRED, the compiler doesn't warn you, and the conditional 
may not be interpreted as was intended.

Best regards
 
David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
 

-Original Message-
From: sc-l-boun...@securecoding.org [mailto:sc-l-boun...@securecoding.org] On 
Behalf Of Bennett, Jason
Sent: 16 February 2009 09:46
To: 'sc-l@securecoding.org'
Subject: Re: [SC-L] Conditional Compile statements-- coding standards,and code 
review

Robert/Sean,

It's a good question and one that I've never seen a really good answer to!
Robert your option certain works but I feel that it somewhat prone to error if 
deployed on a large source base. So for
example if a developer actually
uses:

#ifdef FRED
#  define MACRO(x) (x + 5)
#endif

... then it's quite possible that this is missed by the review team and there 
is of course no guarantee that all code is
reviewed manual. There is also the problem that there may be more than a single 
target release build for different
variants i.e. it's not just a binary choice of release or debug versions.

To make a more 'fool proof' mechanism I believe that it's better to have a more 
controlled use of which pre-processor
directives are allowed for conditional compilation and ensure their use is 
consistent -- this is particular true of
debug information which I believe causes the most problems. Following this 
approach would allow you to perform automatic
searches for directives that are not on a defined white list. A word of warning 
this isn't as easy as it seems once you
start getting statements of the following type -- this just re-enforces the 
problem of conditional
compilation:

#if defined c1  !(defined c2 || defined c3)  ...
#elif defined C4
 ...
#endif

What would be really nice is to have an automatic tool that can check that for 
say build target A you can only have I, J
and K defined but for not L and M -- using 3rd party code which is often 
designed to be ported to multiple targets
sorting out what is actually used is not easy at all!

Use should also looked at carefully to ensure that conditional compilation is 
only used where 'required'. So as an
example do you really want all those call traces and information output used 
during development left in the code?

In conclusion I believe that you should aim for as much automation as possible 
and also taking the problem out of the
developer's hands. It's much easier to ensure that you've done something right 
once in your build system than expect
every developer to do it right every time -- in my experience developers are 
happy to change what is in their 'local
domain' but think about things a bit more carefully if they are making a change 
the can affect the entire development.

Obviously these are just some ideas and I'm sure that there or other equally 
good solutions and as with all these things
it does depend on what level of assurance you want otherwise you get the answer 
of don't allow conditional compilation! 
Consider the environment before printing this mail.
Thales e-Security Limited is incorporated in England and Wales with company 
registration number 2518805. Its registered
office is located at 2 Dashwood Lang Road, The Bourne Business Park, 
Addlestone, Nr. Weybridge, Surrey KT15 2NX.
The information contained in this e-mail is confidential. It may also be 
privileged. It is only intended for the stated
addressee(s) and access to it by any other person is unauthorised. If you are 
not an addressee or the intended
addressee, you must not disclose, copy, circulate or in any other way use or 
rely on the information contained in this
e-mail. Such unauthorised use may be unlawful. If you have received this e-mail 
in error please delete it (and all
copies) from your system, please also inform us immediately on +44 (0)1844 
201800 or email
postmas...@thales-esecurity.com.
Commercial matters detailed or referred to in this e-mail are subject to a 
written contract signed for and on behalf of
Thales e-Security Limited. 
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org List information, 
subscriptions, etc -
http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com) as a 
free, non-commercial service to the
software security community.
___

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http

[SC-L] 5th IEEE International Conference on Software Engineering and Formal Methods

2007-07-29 Thread David Crocker
Hi all,

Seeing that formal methods have been used to prove aspects of system security, I
thought that some members might be interested in the 5th IEEE SEFM conference,
which will be held on 12-14 September in London.

The conference program (http://www.iist.unu.edu/SEFM07/programme.html) includes
papers on the following:

 Verifying the Mondex Case Study (verifying that a smart card money-exchange
protocol is secure)

 Recovery from DoS Attacks in MIPv6

 Verification of C Programs Using Automated Reasoning (my own paper - includes
absence of buffer overflow)

See http://www.iist.unu.edu/SEFM07 for more details.

Regards,

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




___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___


Re: [SC-L] Harvard vs. von Neumann

2007-06-11 Thread David Crocker
Crispin Cowen wrote:


IMHO, all this hand wringing is for naught. To get systems that never fail
requires total correctness. Turing tells us that total correctness is not
decidable, so you simply never will get it completely, you will only get
approximations at best.


What Turing actually tells us is that it is possible to construct programs that
may be correct but whose correctness is not decidable. This is a far cry from
saying that it is not possible to build well-structured programs whose
correctness _is_ decidable.


Having humans write specifications and leaving programming to computers is
similarly a lost cause. At a sufficiently high level, that is asking the
computer to map NP to P, and that isn't going to happen.


I don't understand what you are getting at here. If you are saying that humans
can map NP to P, but that it is impossible in principle to have computers do the
same thing, then that sounds like a religious argument to me. If you are saying
that you can write a specification that is unsatisfiable (or whose
satisfiability is undecidable) and that therefore cannot be implemented as code,
then this applies equally to human programmers. Incidentally, I have heard of a
few cases in which programming teams have wasted effort trying to implement sets
of requirements which, when the requirements were formalised, turned out to be
contradictory.


At a less abstract level, you are just asking the human to code in a higher
level language. This will help, but will not eliminate the problem that you just
cannot have total correctness.


The higher the level in which the human codes, the less mistakes there are to
be made, assuming equal familiarity with the language etc. And you are just
repeating the same fallacious proposition by saying you cannot have total
correctness. Had you instead said you can never be sure that you have
established that the requirements capture the users' needs, I would have had to
agree with you.


Programmable Turing machines are great, they do wonderful things, but total
correctness for software simply isn't feasible. People need to understand that
programs are vastly more complex than any other class of man made artifact ever,
, and there fore can never achieve the reliability of, say, steam engines.


Same old flawed proposition. And, in software, the behaviour of the components
we build programs out of (i.e. machine instructions) are much more well-defined
and reliable than the materials that steam engines are built out of.


The complexity of software is beginning to approach living organisms. People at
least understand that living things are not totally predictable or reliable, and
s**t will happen, and so you cannot count on a critter or a plant to do exactly
what you want. When computer complexity clearly exceeds organism complexity,
perhaps people will come to recognize software for what it is; beyond definitive
analyzability.


Sure, if you develop a complex software system without a good design process
that carefully refines requirements to specifications to design to code - and
propagates changes in requirements down the chain too - then it may be
impossible to meaningfully analyse that software. That is why my approach is to
formalise requirements, write specifications that are proven to satisfy them,
then refine the specification to code - automatically where possible, but with
manual assistance where e.g. a data structure or an algorithm needs to be made
more efficient.


We can never solve this problem. At best we can make it better.


We can never solve the problem of being certain that we have got the
requirements right. I think that one implication for security is that there may
be whole new classes of threats out there that nobody has thought of yet, and
which we therefore can't refer to in the requirements. But we _can_ solve the
problem of ensuring that software meets the stated requirements, as long as
these are well-defined.

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




___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___


Re: [SC-L] Harvard vs. von Neumann

2007-06-11 Thread David Crocker
 to outline, the additional complexity of automatic refinement of
specifications to code can be mitigated, for example through the use of
automated verification. As for compiler reliability: it's now 8 years since I
had to workaround bugs in the C++ compilers that are the primary targets for our
code generator. That is not to say that there are none, just that the
probability that we will hit one is small enough that we don't have to worry
about it outside the critical software markets. People who use low-volume
specialist compilers for some embedded processors may have a different
experience; but the reality for many (most?) of us is that finding a bug in our
executable code that is caused by a faulty compiler is a rare event.

More than forty years ago, we started the move from assembly language
programming to a higher level of abstraction - high level programming
languages. This raised productivity, and almost certainly reduced error rates.
I think the time has come for a shift to an even higher level of abstraction.

This posting has drifted a little more off-topic than I intended, however I do
think it has a direct bearing on security. In order to get secure software, we
need to:

1. Identify security as a requirement of the software right from the start; and
2. Use a development process that ensures that the finished software meets the
requirements.

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




___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___


Re: [SC-L] FW: What's the next tech problem to be solvedin softwaresecurity?

2007-06-10 Thread David Crocker
IMO the real problem is that software developers are still focussed on
programming, not on specification. We should leave programming to computers,
instead of wasting money paying people to do it and hoping that the resulting
system meets user requirements, including some semblance of security.

If instead we pay people to perform the more skilled tasks of establishing
requirements and specifying the systems to meet them, and use computers to
generate programs that meet the specifications, then such things as freedom from
buffer overflow come free of charge. By freedom here, I don't mean the sort of
freedom that comes in safe languages such as Ada and Java - in which the
buffer overflow raises an exception, probably requiring a restart of the
subsystem - but rather, genuine immunity.

Other security issues (like freedom from SQL injection and cross-site scripting
attacks) may not always come free but are relatively easy to add to the
specification, as long as people are aware of the need to do so.

It amazes me that software development techniques have progressed so little in
the last 50 years. In the 1950s we had assembler. This was followed in the 1960s
by high level programming languages. Nearly 50 years later we have... slightly
better high level programming languages. For example, one of the major
languages in use today is C, which is more than 30 years old. The only
significant advance since the invention of C (and Algol before it) is
object-oriented programming - a welcome improvement, but far short of the
paradigm shift that is desperately needed.

Let's stop focussing on the minute detail of the steps that a computer needs to
execute in order to solve a software problem, and turn our attention instead to
describing what the program is supposed to achieve - including its resistance to
hostile input. Until we do so, we will be doing little more than patching up
outdated technology.

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




-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of SC-L Subscriber Dave Aronson
Sent: 07 June 2007 13:53
To: SC-L@securecoding.org
Subject: Re: [SC-L] FW: What's the next tech problem to be solvedin
softwaresecurity?


Michael S Hines [mailto:[EMAIL PROTECTED] writes:

  Product integration - why have an editor, separate source code analizer,  
separate 'lint' product, compiler, linker, object code analyzer, Fuzz
  testing tools, etc...apart from marketing and revenue stream - it
  doesn't help the developer any.

It may.  IME, all-in-one products usually integrate the pieces well.  On the
other claw, they don't tend to do most, if any, of the pieces well.  On the
third hand, integration doesn't have to mean they're no longer separate.
They can play nicely together if they adhere to relevant standards for
interoperability.  Witness how you can develop a lot of software without leaving
Emacs, or Eclipse.

However, I don't think that's all that relevant to software security in
particular, as opposed to software development in general.

-Dave

-- 
Dave Aronson
Specialization is for insects.  -Heinlein
Work: http://www.davearonson.com/
Play: http://www.davearonson.net/



___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com) as a
free, non-commercial service to the software security community.
___


___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___


Re: [SC-L] Could I use Java or c#? [was: Re: re-writingcollege books]

2006-11-11 Thread David Crocker
Hi Attila,

I wouldn't worry about not being able to see the assembly code while debugging.
In practice, there is less need for debugging Java or C# code than with C++. For
example, in C++, out-of-bounds array writes and incorrect type conversions can
give rise to bugs that are hard to find, because the effect may be felt some
time after the cause (e.g. the out-of-bounds array write corrupts some data). In
Java or C#, the runtime system catches this sort of bug immediately.

My company uses a code generator that can generate either C++ or Java. Although
the production version of the products we ship are built using C++ code, for
development and initial testing we generally use the Java code because bugs are
caught much earlier.

The performance improvement you can get from using C++ rather than Java or C# is
significant only if the program uses really huge amounts of CPU time, in which
case you might be able to make a case that the hardware cost saving outweighs
the higher cost and time to develop in C++ rather than Java or C#. Otherwise,
for application-level programming, Java or C# would generally be a more
productive choice.

Regards

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



-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of SZALAY Attila
Sent: 09 November 2006 11:20
To: [EMAIL PROTECTED]
Cc: Secure Coding
Subject: Re: [SC-L] Could I use Java or c#? [was: Re: re-writingcollege books]


Hi All,

On Thu, 2006-11-09 at 10:20 +1100, mikeiscool wrote:
 
 You can definately get appropriate information via the stack trace 
 with java's exception handling. It's strange to see you say debugging 
 is _eaiser_ in c, typically people find it far easier in a managed 
 language :)

People are different. :))

I personally want to know what happens and I don't believe anything waht I can't
see. In C I can see the assembly code what (I hope) is a deterministic thing. An
interpreter is to big (to me) to think about it as a deterministic thing. And
yes, with ``normal'' bugs a managed language could give me more possibility to
find the place of the problem. But I want to hope, that we don't commit normal
bugs. :)

And with mysterious bugs, when you cannot reproduce it in a test system, just
the costumer some hundred miles away, I think that the stability of the compiled
code (and the core file what may created) is give more more chance to find the
right place.

 That's a java applet; please don't judge Java the language based on 
 applets; they are a really bad representation. Serverside java will be 
 very effective and useful; what sort of client are you writing? Is it 
 a website or a desktop app? Even if it's a desktop app, perhaps look 
 to azureus to see a good, well running app written in java for the 
 desktop. There are others.

This is a desktop application in a client-server model.
I will look after azureus.


___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


Re: [SC-L] re-writing college books [was: Re: A banner year for software bugs | Tech News on ZDNet]

2006-11-04 Thread David Crocker
Crispin,

It is most certainly true that C++ can be appropriate in those cases. C++
programs can perform just as well as C programs, while also being much better
structured. Of course, it will be necessary to avoid performing frequent
allocation and deallocation of heap memory in the C++ program - but the same is
true of C programs. Poorly-performing programs can be written in either
language.

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



-Original Message-
From: Crispin Cowan [mailto:[EMAIL PROTECTED] 
Sent: 03 November 2006 04:46
To: David Crocker
Cc: 'Secure Coding'
Subject: Re: [SC-L] re-writing college books [was: Re: A banner year for
software bugs | Tech News on ZDNet]


David Crocker wrote:
 Unfortunately, there are at least two situations in which C++ is a 
 more suitable alternative to Java and C#:

 - Where performance is critical. Run time of C# code (using the faster 
 .NET 2.0
 runtime) can be as much as double the run time of a C++ version of the same
 algorithm. Try telling a large company that it must double the size of its
 compute farms so you can switch to a better programming language!

 - In hard real-time applications where garbage collection pauses 
 cannot be tolerated.
   
Except that in both of those cases, C++ is not appropriate either. That is a
case for C.

Crispin

-- 
Crispin Cowan, Ph.D.  http://crispincowan.com/~crispin/
Director of Software Engineering, Novell  http://novell.com
 Hack: adroit engineering solution to an unanticipated problem
 Hacker: one who is adroit at pounding round pegs into square holes

___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


[SC-L] Proving the security properties of transaction protocols - 10 years on

2006-10-30 Thread David Crocker
Members of this list might be interested in an article in this month's IEEE
Computer Journal about the use of automatic and semi-automatic theorem proving
to prove the security of a transaction protocol. The article - which is called
First Steps in the Verified Software Grand Challenge - concerns the transaction
protocol that was used by the Mondex electronic purse, which was developed and
formally verified (by hand) around ten years ago. Several teams have recently
attempted to apply modern tools to the problem. In the process, several of the
teams working on the project found that the original hand-developed proof was
incomplete, but could be patched.

More details can be found at
http://csdl2.computer.org/persagen/DLAbsToc.jsp?resourcePath=/dl/mags/co/toc=co
mp/mags/co/2006/10/rxtoc.xmlDOI=10.1109/MC.2006.340#abstract . Non-subscribers
can download the article for $19.

My own company provided one of the teams working on this problem, and we found
it is quite a challenge to prove the protocol correct by fully-automatic means.
Proofs that software is free from buffer overflows for all possible inputs are
almost trivial by comparison.

Regards

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



___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


Re: [SC-L] re-writing college books [was: Re: A banner year for software bugs | Tech News on ZDNet]

2006-10-29 Thread David Crocker
Crispin Cowan wrote:


For me, the enemy in the room is C++. It gives you the safety of C with the
performance of SmallTalk. There is no excuse at all to be writing anything in
C++ yet vastly too many applications are written in C++ anyway. Instead of
trying to coax developers to switch from C++ to something weird like SML, lets
encourage them to switch to Java or C#, which are closer to their experience.


Unfortunately, there are at least two situations in which C++ is a more suitable
alternative to Java and C#:

- Where performance is critical. Run time of C# code (using the faster .NET 2.0
runtime) can be as much as double the run time of a C++ version of the same
algorithm. Try telling a large company that it must double the size of its
compute farms so you can switch to a better programming language!

- In hard real-time applications where garbage collection pauses cannot be
tolerated.

However, I suspect that most security-critical programs do not fall into either
of these categories, so C# or Java would indeed be a better choice than C++ for
those programs.

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



___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


Re: [SC-L] How can we stop the spreading insecure codingexamplesattraining classes, etc.?

2006-09-01 Thread David Crocker
Also, exceptions (unlike gotos) cannot be used to jump backward, thereby
creating hidden loops.

Used correctly, exceptions eliminate large amounts of code that would otherwise
be required to handle unexpected failures at every level in a function call
stack and propagate such failures upwards by way of return codes etc. to a point
at which some remedial action can be taken. Exceptions can certainly be misused,
but they are much better than the alternatives in many situations.

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



-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of der Mouse
Sent: 31 August 2006 22:45
To: SC-L@securecoding.org
Subject: Re: [SC-L] How can we stop the spreading insecure
codingexamplesattraining classes, etc.?


 ever heard of exceptions?  They're basically goto plus limited state.  
 Spaghetti lives!

Not at all.  Exceptions are not like gotos; in particular, an exception cannot
be used to jump *into* a construct.  The major problems with gotos are that they
can be used to do branches that are downward or sideways in the code parse tree
(versus structured constructs, which do such branches upward only).
Exceptions are upward-only branches, and as a result don't have most of the
problems gotos do.

/~\ 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
___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php


RE: [SC-L] Java keystore password storage

2005-04-25 Thread David Crocker
I'm by no means an expert in the field of security and Java, but I believe that
the usual technique is to encode the password that the user types using a 1-way
hashing algorithm, then store (and hide/protect) the encoded version and use
that as the password. If an attacker manages to read the password hash, he still
has to construct a password that will encode to the same value.

There are a number of hashing algorithms available. SHA1 used to be considered
fairly good for this sort of thing, but I understand it has been broken
recently.

This technique does make it impossible to recover the password; if the password
is lost, it has to be reset to a new one.

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



-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf
Of john bart
Sent: 25 April 2005 08:56
To: SC-L@securecoding.org
Subject: [SC-L] Java keystore password storage


Hello to all the list.
I need some advice on where to store the keystore's password. Right now, i have
something like this in my code:

keystore = KeyStore.getInstance(JKS);
keystore.load(new FileInputStream(keystore.jks),PASSWORD);

the question is, where do i store the password string? all of the possibilities
that i thought about are not good enough:
1) storing it in the code - obviously not.
2) storing it in a seperate config file is also not secure.
3) entering the password at runtime is not an option.
4) encrypting the password - famous chicken and egg problem (storing the
encryption key)

Any ideas?





RE: [SC-L] Theoretical question about vulnerabilities

2005-04-14 Thread David Crocker
Crispin wrote:

 Here's an example of a case it cannot prove:

if X then
Y - initial value
endif
...
if X then
Z - Y + 1
endif

The above code is correct in that Y's value is taken only when it has
been initialized. But to prove the code correct, an analyzer would have
to be flow sensitive, which is hard to do.


The whole science of program proving is based on exactly this sort of flow
analysis. The analyser will postulate that Y is initialised at the assignment to
Z, given the deduced program state at that point. This is called a verification
condition or proof obligation. It can then attempt to prove the hypothesis;
for this example, the proof is trivial. I guess it would have been more
difficult 20 years ago when Hermes was written.

The alternative solution to the problem of uninitialised variables is for the
language or static checker to enforce Java's definite initialisation rule or
something similar. This at least guarantees predictable behaviour.

An issue arises when a tool like Perfect Developer is generating Java code,
because even though PD can prove that Y is initialised before use in the above
example, the generated Java code would be violate the definite initialisation
rule. We have to generate dummy initialisations in such cases.

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



RE: [SC-L] Theoretical question about vulnerabilities

2005-04-14 Thread David Crocker
Crispin Cowan wrote:


Precisely because statically proven array bounds checking is Turing Hard, that
is not how such languages work.

Rather, languages that guarantee array bounds insert dynamic checks on every
array reference, and then use static checking to remove all of the dynamic
checks that can be proven to be unnecessary. For instance, it is often the case
that a tight inner loop has hard-coded static bounds, and so a static checker
can prove that the dynamic checks can be removed from the inner loop, hoisting
them to the outer loop and saving a large proportion of the execution cost of
dynamic array checks.


Well, that approach is certainly better than not guarding against buffer
overflows at all. However, I maintain it is grossly inferior to the approach we
use, which is to prove that all array accesses are within bounds. What exactly
is your program going to do when it detects an array bound violation at
run-time? You can program it to take some complicated recovery action; but how
are you going to test that? You can abort the program (and restart it if it is a
service); but then all you have done is to turn a potential security
vulnerability into a denial of service vulnerability.

So the better approach is to design the program so that there can be no buffer
overflows; and then verify through proof (backed up by testing) that you have
achieved that goal.

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



RE: [SC-L] Theoretical question about vulnerabilities

2005-04-11 Thread David Crocker
Pascal Meunier wrote:


Do you think it is possible to enumerate all the ways all vulnerabilities can be
created?  Is the set of all possible exploitable programming mistakes bounded?


No. It's not so much a programming problem, more a specification problem.

Tools now exist that make it possible to develop single-threaded programs that
are mathematically proven to meet their specifications. The problem is knowing
what should be included in the specifications. Let me give you some examples:

1. Buffer overflow. Even if nobody realised that buffer overflows could be used
to bypass security, it is an implied specification of any program that no array
should ever be accessed via an out-of-bounds index. All the tools out there for
proving software correctness take this as a given. So buffer overflows can
always be avoided, because if there is ANY input whatsoever that can produce a
buffer overflow, the proofs will fail and the problem will be identified. You
don't even need to write a specification for the software in this case - the
implied specification is enough.

2. SQL injection. If the required behaviour of the application is correctly
specified, and the behaviour of the SQL server involved is also correctly
specified (or at least the correct constraints are specified for SQL query
commands), then it will be impossible to prove the software is correct if it has
any SQL injection vulnerabilities. So again, this would be picked up by the
proof process, even if nobody knew that SQL injection can be used to breach
security.

3. Cross-site scripting. This is a particular form of HTML injection and would
be caught by the proof process in a similar way to SQL injection, provided that
the specification included a notion of the generated HTML being well-formed. If
that was missing from the specification, then HTML injection would not be
caught.

4. Tricks to make the browser display an address in the address bar that is not
the address of the current HTML page. To catch these, you would need to include
in the specification, the address bar shall always show the address of the
current page. This is easy to state once you know it is a requirement; but
until last year it would probably not have been an obvious requirement.

In summary: If you can state what you mean by secure in terms of what must
happen and what must not happen, then by using precise specifications and
automatic proof, you can achieve complete security for all possible inputs -
until the definition of secure needs to be expanded.


This should have consequences for source code vulnerability analysis software.
It should make it impossible to write software that detects all of the mistakes
themselves.  Is it enough to look for violations of some invariants (rules)
without knowing how they happened?


The problem is that while you can enumerate the set of invariants that you
currently know are important, you don't know how the set may need to be expanded
in the future.

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



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

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

2004-07-10 Thread 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 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.

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

2004-07-09 Thread David Crocker
Crispin Cowan wrote:


In programming language terms, Ada is grossly primitive. Its object
orientation mechanisms are crude at best. A *great* deal of progress in
language technology has been made since Ada was developed. For just
about any kind of concept or safety feature, students and developers
would be better served to consider Java, C#, or ML instead of Ada.


I'm no fan of Ada (I find the language cumbersome and verbose, and it makes a
pigs ear of trying to be fully O-O) - but I have to defend Peter Amey in this
case.

There is a tendency to regard every programming problem as an O-O problem.
Sometime last year I read a thread on some programming newsgroup in which
contributors argued about the correct way to write a truly O-O Hello world
program. All the solutions provided were cumbersome compared to the traditional
printf(Hello, world!) solution. The point is, printing Hello, world! is
not an O-O problem!

Although for most commercial application packages an O-O architecture is the
best choice at present, for many embedded systems there is absolutely no reason
to use polymorphism with dynamic binding - which are the main language features
that distinguish the O-O approach from earlier methods. Ada has always provided
the other benefits associated with O-O languages (encapsulation, information
hiding, genericity). In safety-critical work there is a good case for regarding
dynamic binding as dangerous unless you formally prove it to be safe using
rigorous methods. And much as I dislike Ada, I have to admit that if you don't
intend to use dynamic binding and don't need the low-level features of C, Ada is
one of the safest languages around.

BTW there is probably more embedded programming being done using C rather than
anything more modern. Java is ruled out for most real-time embedded applications
because garbage collection pauses cannot be tolerated. [My own preference for
embedded work is MISRA C extended with a few features from C++ - but it needs
good tool support in order to ensure that all the worst unsafe features of C/C++
are avoided.]


Java, C#, and ML are strictly better than Pascal and Ada for almost
everything. But they did not spring out of the earth, they were built on
the progress of previous languages. Java in particular contains no novel
features at all, but rather shows good taste in the features it borrows
from others. What made Java interesting was the accident of history that
caused it to become the first strongly typed polymorphic programming
language to become widely popular.


I disagree with your almost everything because there is a huge amount of
embedded software developed for which Java is unsuitable. Java is certainly a
big improvement on C++ for anyone not needing the low-level control that C++ can
give, but unfortunately the designers of Java still borrowed too much from
C/C++. In particular, mixing automatic type conversion with overloading is a
_very_ bad idea. Indeed, for safety-critical work, almost any sort of automatic
type conversion is a very bad idea. The depressing thing about Java is that it
contains almost nothing new. In contrast, the designers of Eiffel added language
features designed to make producing correct programs easier.


You *can* teach object orientation with Simula 67 or SmallTalk, if you
really want to. But teaching object orientation with Java is a lot more
approachable in the contemporary context.


I certainly wouldn't advocate teaching Simula or Smalltalk. But focussing solely
on Java and O-O programming does not set students up well for embedded software
development.

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






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

2004-07-09 Thread 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] opinion, ACM Queue: Buffer Overrun Madness

2004-06-11 Thread David Crocker
ljknews wrote:


And there are ways of using Assembly Language to avoid pitfalls that it
provides.  There are ways of using horse-drawn carriages to avoid the
major reason (think street cleaning) why the automobile was embraced in
urban areas during the early part of the 20th century.

What there are _not_ are reasons for new development to cling to languages
which make flawed constructs easy for the individual programmer to misuse.


There is often one very good reason for clinging to such languages: because
there is no other suitable language available. As has already been pointed out,
there is usually very little alternative to C/C++ when it comes to kernel mode
code.

I would love to see a safer alternative to C/C++ for writing operating system
kernels, device drivers and real-time embedded applications (yes, I know Ada can
be used for the latter, buts its package structure and associated with-ing
problem can be a real pain in large systems). The newer programming languages
such as Java, C# and Eiffel are all designed for applications and make heavy use
of garbage collection (which is a boon to application writers, but a no-no for
kernel code and many embedded apps).

What I don't understand is why the language standardisation committees don't
remove some of the unsafe dross when they bring out new language revisions. A
classic example is the failure to define the type of a string literal in C as
const char*. Just imagine if we had a new version of C++ with all the unsafe
stuff removed. Backwards compatibility would not be a problem in practice,
because the compiler suppliers would provide switches to make their new
compilers accept obsolete constructs.

As for non-real-time application-level code, I gave up writing them in C++ by
hand long ago. [Actually I prefer to write specifications, verify them, and let
a code generator produce correct C++ from them; but that is another story.]

David Crocker
Consultancy  contracting for dependable software development
www.eschertech.com






RE: [SC-L] opinion, ACM Queue: Buffer Overrun Madness

2004-06-09 Thread David Crocker
Sloppy coding can be done in any language, but C and C++ have 3 features that
aggravate the problem:

1. The array=pointer idiom. Given a parameter which is an array, you can't ask
at run-time how big the array is - you have to do extra work and pass the size
in an additional parameter (whereas most languages pass the size of an array
automatically as part of the array). So doing buffer overflow checks requires
more than just inserting the check - you have to make sure that an extra array
size parameter is passed all the way down the call stack. [C and C++ cannot be
considered strongly typed, in part because of the lack of distinction between
pointers and arrays].

2. By permitting pointer arithmetic, C and C++ encourage you to pass a pointer
into the middle of a buffer, rather than passing the [start of the] buffer and
an index into it, which makes bounds checking even more tedious to do (you have
to pass a pointer to one-past-the-end-of-the-array as well, and even then this
is less useful than having an index and a limit).

3. The lack of automatic bounds checking. Of course, run-time bounds checking is
by no means a complete solution, but it does at least prevent a buffer overflow
being used as a security attack, turning it into a denial-of-service attack
instead.

Apart from the obvious solution of choosing another language, there are at least
two ways to avoid these problems in C++:

1. Ban arrays (to quote Marshall Cline's C++ FAQ Lite, arrays are evil!). Use
classes from the STL, or another template library instead. Arrays should be used
only in the template library, where their use can be controlled.

2. If you really must have naked arrays, ban the use of indexing and arithmetic
on naked pointers to arrays (i.e. if p is a pointer, then p[x], p+x, p-x, ++p
and --p are all banned). Instead, refer to arrays using instances of a template
class ArrayX that encapsulates both the pointer (an X*) and the limit (an
unsigned int). Such an object needs only 2 words of storage (compared to 1 word
for a naked pointer), so it can assigned and passed by value. You can provide an
operator to return the value of the limit, and an indexing operator (with
optional bounds checking). If you really must, you can even implement pointer
arithmetic operators for the class which update the limit at the same time as
updating the pointer.

David Crocker
Consultancy  contracting for dependable software development
www.eschertech.com