Idea: Array Boundary Checks on Write Access Only

Idea: Array Boundary Checks on Write Access Only

[Markus Kuhn]

Here is a suggestion for Ada compiler developers:

Add a compiler configuration option that suppresses array index
boundary checks only for *read* access to array elements.

Array boundary checks in Ada are a major advantage over C/C++
and add a lot to the safety and debugability of the language.
However the checks are also a significant performance loss
unless they are deactivated. A useful compromise would be an
option that causes the compiler to add boundary checks only
when an array element is written, but not when it is read.
Out-of-boundary array write accesses are dangerous because they can
destroy other data structures and can cause failure inside completely
unrelated objects. Therefore, in security critical applications,
it is very desireable to deactivate for performance reasons
only the checks for the less dangerous read accesses that if
they go wrong should not cause malfunction within other objects.

Are there already Ada compilers around that do this?

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>

Re: Idea: Array Boundary Checks on Write Access Only

[Peter Amey]

Markus Kuhn wrote:
> 
> Here is a suggestion for Ada compiler developers:
> 
> Add a compiler configuration option that suppresses array index
> boundary checks only for *read* access to array elements.
> 
> Array boundary checks in Ada are a major advantage over C/C++
> and add a lot to the safety and debugability of the language.
> However the checks are also a significant performance loss
> unless they are deactivated. A useful compromise would be an
> option that causes the compiler to add boundary checks only
> when an array element is written, but not when it is read.
> Out-of-boundary array write accesses are dangerous because they can
> destroy other data structures and can cause failure inside completely
> unrelated objects. Therefore, in security critical applications,
> it is very desireable to deactivate for performance reasons
> only the checks for the less dangerous read accesses that if
> they go wrong should not cause malfunction within other objects.
> 
> Are there already Ada compilers around that do this?
> 
> Markus

Working in the safety-critical, real-time field I frequently encounter the 
tension between the need for checking and the desire for speed.  Another 
factor is the need to generate very high levels of object-code test coverage 
to satisfy some regulatory regimes; this is rather hard if the compiler has 
inserted run-time checks that in practice are unncessary and therefore 
cannot be externally stimulated.  In this environement I am not very happy 
with the idea that reading out of bounds is any less unsatisfactory than 
writing: both show that the code is broken and may misbehave.  

It was to square this particular circle that we invested so much effort in 
the proof of absence of run-time errors facility in SPARK (Markus, I know 
you are familiar with this...).   Having conducted a proof that code is 
exception free it is possible to turn compiler-generated checks off with a 
clear conscience and get the benefit of smaller, faster code as a bonus.

Peter

-- 
--------------------------------------------------------------------------- 
  
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/
 --------------------------------------------------------------------------

Re: Idea: Array Boundary Checks on Write Access Only

[Markus Kuhn]

Stephen Leake wrote:
> I don't see why a "read bug" is ever ok!

An array read bug has only local consequences, a wrong return
result (unless the result is an erroneous pointer). An array or
pointer write bug can cause erroneous behaviour in other completely
indepentent classes even if the implementation of these is carefully
scrutinized to be bug free and very carefully shielded against
wrong parameters.

There are no bug free systems but in many types of systems, some
modules (e.g., an encryption module that must not leak secret
keys) must be especially carefully reviewed, while the huge majority
of the system is much less critical. This some-modules-only
review makes only sense if there is a guarantee that no other
less pedantically reviewed code (user interface, etc.) can
accidentially or maliciously be caused to overwrite the internal data
structures of the critical module.

Therefore, array boundary checks for write access are much more
important than array boundary checks for read access, and I think
it is a cute idea to be able to switch off read checks and leave
in write checks for production versions. Read checks should
however stay in effect for pointer arrays, when to the target
of the read pointer a later write access might happen.

A wrong array read just causes some variable value to be wrong,
there are thousands of other bugs that have the same effect. A
wrong array or pointer write causes errors at other places and
that is an effect other types of bugs will not have.

So I think write-only checks are a useful tradeoff in many
situations. The read checks are very expensive, not only because of
the inserted check instructions, but also because the many
different paths of execution that can result make optimization
difficult.

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>

Re: Idea: Array Boundary Checks on Write Access Only

[Robert A Duff]

Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> writes:

> An array read bug has only local consequences, a wrong return
> result (unless the result is an erroneous pointer). An array or
> pointer write bug can cause erroneous behaviour in other completely
> indepentent classes even if the implementation of these is carefully
> scrutinized to be bug free and very carefully shielded against
> wrong parameters.

But integers behave just like pointers, when used as array indices:

    type Int_1_10 is range 1..10;
    type A is array(Int_1_10) of Boolean;
    A_Obj: A;
    
    type B is array(Integer range 1..3) of Int_1_10;
    B_Obj: B := (others => 1);
    
    ... -- lots of code that might change B_Obj, but it's all properly
        -- range-checked, so we know B_Obj(I) is in 1..10, for all I.

Then:
    X: Integer := 1_000_000;
    ... -- might change X
    Y: Int_1_10 := B_Obj(X);
    A_Obj(Y) := True;

With checks turned on, there will be a check on B_Obj(X), to make sure X
is in 1..3.  A good compiler will notice that the result of B_Obj(X)
must be in 1..10, so no check is needed on the assignment to Y, and
likewise no check is needed on A_Obj(Y), since Y must be in 1..10.  But
if we eliminate the check on B_Obj(X), which is a *read*, we end up
doing an evil *write*.  The assignment to A_Obj(Y) will modify some
random bit in memory -- who knows where.

So "reads" aren't so harmless after all.

On the other hand, if we make a rule that the elimination of the first
check must cause the re-insertion of the second check, then it's not
clear what efficiency we've gained.

> There are no bug free systems but in many types of systems, some
> modules (e.g., an encryption module that must not leak secret
> keys) must be especially carefully reviewed, while the huge majority
> of the system is much less critical. This some-modules-only
> review makes only sense if there is a guarantee that no other
> less pedantically reviewed code (user interface, etc.) can
> accidentially or maliciously be caused to overwrite the internal data
> structures of the critical module.

It seems to me that you can't know that, unless the two modules are in
separate address spaces with hardware memory protection preventing
inter-module naughtiness.  No matter how carefully you review module A,
someone can break it accidentally or maliciously in a totally-unrelated
module B, by using any number of unsafe features (such as unchecked
conversion of pointers, machine code insertions, address clauses, &c).
Assuming A and B share the same address space, that is.

- Bob

-- 
Change robert to bob to get my real email address.  Sorry.
-- 
Change robert to bob to get my real email address.  Sorry.

Re: Idea: Array Boundary Checks on Write Access Only

[Stephen Leake]

Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> writes:

> Here is a suggestion for Ada compiler developers:
> 
> Add a compiler configuration option that suppresses array index
> boundary checks only for *read* access to array elements.
> 
> Array boundary checks in Ada are a major advantage over C/C++
> and add a lot to the safety and debugability of the language.
> However the checks are also a significant performance loss
> unless they are deactivated. A useful compromise would be an
> option that causes the compiler to add boundary checks only
> when an array element is written, but not when it is read.
> Out-of-boundary array write accesses are dangerous because they can
> destroy other data structures and can cause failure inside completely
> unrelated objects. Therefore, in security critical applications,
> it is very desireable to deactivate for performance reasons
> only the checks for the less dangerous read accesses that if
> they go wrong should not cause malfunction within other objects.

A bug is a bug. If you write your code with properly typed indices, a
good compiler can optimize away all array index checks, at least for
statically sized constrained arrays. If you are using true dynamically
sized or unconstrained arrays, you either need to have the compiler do
all the checks, or do them all yourself somewhere. In the later case,
you can turn off the compiler checks.

I don't see why a "read bug" is ever ok!

> 
> Are there already Ada compilers around that do this?

I hope not :).

> 
> Markus
> 

-- Stephe

Re: Idea: Array Boundary Checks on Write Access Only

[Markus Kuhn]

Lieven Marchand wrote:
> About the only commonly used case that most compilers don't handle is
> where you put in the check yourself.

It would be really neat if Ada compilers would keep track not only of
the declared range of a subtype, but also of the effectively possible
range of Integer variables inside a certain program fragment as part
of the flow analysis.

For instance in code such as

  if J > 0 then
     -- compiler notes that here J : range 1 .. J'Last
     if I > J then
        -- compiler notes that here I : range 1 .. I'Last

then the compiler should know that inside the second "if" I > 0 always
holds. This need not be a full blown automatic proof system, just some
logic that understands simple inequalities and monotonic expressions
and that keeps track of the effective maximum and minimum value
of integer variables and supresses most checks accordingly.

It would then also be a nice option if the compiler would be
able to dump a list of all the checks that it still had to insert
to give developers a clue of whether they can by intelligently
placing a manual check at the right place make a large number
of automatically inserted less efficient checks unnecessary.

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>

Re: Idea: Array Boundary Checks on Write Access Only

[Stuart Palin]

Markus Kuhn wrote:
> 
> Stephen Leake wrote:
> > I don't see why a "read bug" is ever ok!
> 
> An array read bug has only local consequences, a wrong return

Not necessarily so; two counter-examples spring to my mind:

1) A read access outside the permissible memory bounds for the
   process causing an Operating System generated access violation
   which results in the whole process being terminated.

   This sort of problem might occur on a multi-user computer system
   (e.g. VAX) the operating system has a need to protect independent
   processes; or even on 'embedded' systems where a security policy
   is enforced by the OS.

2) The read may access memory mapped hardware devices and may cause
   the device to react; for example an IO device may assume that
   the last set of data has been accessed and it initiates the next
   IO transaction - resulting in lost data.

   This sort of problem might occur in embedded system where elaborate
   protection mechanisms (see case 1 above) are not built into the
   system.

It would be possible to design systems that avoid both these problems
(ie hardware access requires the software to be operating in a
'privileged' mode and for any violations of memory constraints to be
'silently' ignored and some hack value returned) - but this is by no
means typical of systems in use.

As you also note, there are other ways in which incorrect read accesses
can lead to subsequent memory access violations (reading an array of
pointers); unfortunately once you open this pandora's box it can quickly
become very difficult to manage the risks.  You mention retaining checks
on arrays of pointers; what if the array returns a loop termination
condition - the program may go into an infinite loop.  If the value is
used in a jump table (a common implementation of 'case' statements) the
program control flow becomes unpredicatable (it could even execute data
- so you may end up running a different program).

Once you allow data to become erroneous (through whatever means) it
quickly undermines many of the premises on which the whole behaviour of
the program is built.  Ada compilers in particular are allowed to assume
that variables conform to their type declaration and optimise
accordingly.  Ada's premise is that a constraint error would be raised
if you tried to give a variable a value outside that range.  If you
suppress that check (anywhere) you risk creating an erroneous program.


All that said the original idea is not entirely without merit, the
issues of performance that Markus mentions are all too real in many
systems.  Generally though I think it is preferable to prove that you do
not have an erroneous program and with Ada's strong typing it is
possible to write code that is easier for a compiler to optimise,
allowing it to remove unnecessary run-time checks where the rules of the
language make it clear that an error can not occur.

As Peter Amey notes regarding the work done with SPARK - proving the
absence of errors, rather than living with them and assuming their scope
for causing damage is limited, is generally more sound.

--
Stuart Palin
Consultant Engineer
Flight Systems Division (Rochester)
GEC-Marconi Avionics Ltd

Re: Idea: Array Boundary Checks on Write Access Only

[Stuart Palin]

Markus Kuhn wrote:
> 
> Lieven Marchand wrote:
> > About the only commonly used case that most compilers don't handle is
> > where you put in the check yourself.
> 
> It would be really neat if Ada compilers would keep track not only of
> the declared range of a subtype, but also of the effectively possible
> range of Integer variables inside a certain program fragment as part
> of the flow analysis.

<snip>

The Praxis Critical Systems work with SPARK has recognised this need for
'shallow-proofs' and they have some very interesting ideas and the tool
support to back it up.

Try looking at http://www.praxis-cs.co.uk/

--
Stuart Palin
Consultant Engineer
Flight Systems Division (Rochester)
GEC-Marconi Avionics Ltd

Re: Idea: Array Boundary Checks on Write Access Only

[Anonymous]

<35851B64.5BF271C4@cl.cam.ac.uk> <ug1h4ylhp.fsf@gsfc.nasa.gov>

On Wed, 17 Jun 1998 18:38:12 +0000, Markus Kuhn
<Markus.Kuhn@cl.cam.ac.uk> wrote:

[arguing for allowing array read checks to be turned off while retaining
array write checks]

> ...
> There are no bug free systems but in many types of systems, some
> modules (e.g., an encryption module that must not leak secret
> keys) must be especially carefully reviewed, while the huge majority
> of the system is much less critical. This some-modules-only
> review makes only sense if there is a guarantee that no other
> less pedantically reviewed code (user interface, etc.) can
> accidentially or maliciously be caused to overwrite the internal data
> structures of the critical module.
> ...

This example seems to disprove your argument. Let us assume a system
with an encryption module that contains secret keys which must not leak,
and some other, non-critical module. A formal analysis of the encryption
module proves that it is error free. No analysis is done of the
non-critical module. Array read checks are disabled for the system, but
array write checks are retained.

The absence of array read checks means that

type T is array (Positive range 1 .. 10) of Integer;
A : T;
B : Integer;
I : Integer;
..
I := -10;
..
B := A (I);

will execute without raising an exception. B will be assigned the value
of some storage prior to A in memory, interpreted as an Integer. I will
call such an array read outside the array boundaries as a "wild read".

The developer of the non-critical module is aware of the encryption
module and interested in knowing what the actual secret key values are.
To that end, he studies the memory layout of the executable to determine
where in memory the secret keys are stored, and inserts wild reads into
the non-critical module intended to read the secret keys. He is
successful and is able to transfer money from other peoples' bank
accounts into his own as a result.

Thus we see that eliminating array index range checks only on array
reads has been able to circumvent the safety of the encryption module,
despite the formal analysis proving its correctness. Had read checks
also been in effect, this could not have happened.

Jeff Carter  PGP:1024/440FBE21
My real e-mail address: ( carter @ innocon . com )
"Hello! Smelly English K...niggets."
Monty Python & the Holy Grail

Posted with Spam Hater - see
http://www.compulink.co.uk/~net-services/spam/

Re: Idea: Array Boundary Checks on Write Access Only

[dennison]

In article <3588D738.4BB32E5A@cl.cam.ac.uk>,
  Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> wrote:
>
> It would be really neat if Ada compilers would keep track not only of
> the declared range of a subtype, but also of the effectively possible
> range of Integer variables inside a certain program fragment as part
> of the flow analysis.

Quite a few compilers are capable of this kind of optimization. I suspect that
includes Ada compilers.

> It would then also be a nice option if the compiler would be
> able to dump a list of all the checks that it still had to insert
> to give developers a clue of whether they can by intelligently
> placing a manual check at the right place make a large number
> of automatically inserted less efficient checks unnecessary.

That kind of "with help I could optimize better" feedback is still pretty
rare.

-----== Posted via Deja News, The Leader in Internet Discussion ==-----
http://www.dejanews.com/   Now offering spam-free web-based newsreading

Re: Idea: Array Boundary Checks on Write Access Only

[dennison]

In article <3588D738.4BB32E5A@cl.cam.ac.uk>,
  Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> wrote:
>
> It would be really neat if Ada compilers would keep track not only of
> the declared range of a subtype, but also of the effectively possible
> range of Integer variables inside a certain program fragment as part
> of the flow analysis.

Quite a few compilers are capable of this kind of optimization (remember, most
compiler optimization research has been targetted towards weakly-typed
languages like Fortran). I suspect that many (perhaps most) Ada compilers can
do this.

> It would then also be a nice option if the compiler would be
> able to dump a list of all the checks that it still had to insert
> to give developers a clue of whether they can by intelligently
> placing a manual check at the right place make a large number
> of automatically inserted less efficient checks unnecessary.

That kind of "with help I could optimize better" feedback is still pretty
rare. Anyway, for what you are looking for, dissasembly of the object code in
the debugger would probably suit your purposes just fine.

-----== Posted via Deja News, The Leader in Internet Discussion ==-----
http://www.dejanews.com/   Now offering spam-free web-based newsreading

Re: Idea: Array Boundary Checks on Write Access Only

[Lieven Marchand]

Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk> writes:

> Lieven Marchand wrote:
> > About the only commonly used case that most compilers don't handle is
> > where you put in the check yourself.
> 
> It would be really neat if Ada compilers would keep track not only of
> the declared range of a subtype, but also of the effectively possible
> range of Integer variables inside a certain program fragment as part
> of the flow analysis.
> 
> For instance in code such as
> 
>   if J > 0 then
>      -- compiler notes that here J : range 1 .. J'Last
>      if I > J then
>         -- compiler notes that here I : range 1 .. I'Last
> 
> then the compiler should know that inside the second "if" I > 0 always
> holds. This need not be a full blown automatic proof system, just some
> logic that understands simple inequalities and monotonic expressions
> and that keeps track of the effective maximum and minimum value
> of integer variables and supresses most checks accordingly.
> 

Actually, most algorithms for this kind of thing would do that. Check
out "Elimination of Redundant Array Subscript Range Checks" from
P. Kolte and M. Wolfe for a nice introduction to this stuff. It's
available on the web from cse.ogi.edu but I haven't got the URL
handy. They cite the Alsys and Karlsruhe Ada compiler as previous
work. In their examples (with Fortran) they eliminate typically 98% of
the checks that a naive implementation inserts but I have the feeling
this would be too optimistical in general.  Earlier work by Gupta
using a slightly different approach gives elimination percentages from
52 to 100 with typical values around 80-90.

One of the problems in doing this with Ada is that the language spec
describes the exact behaviour for errors like this. You have to raise
the correct exception after having done all the previous effects. This
restricts the freedom of the compiler to rearrange checks. In
languages with similar semantics for arrays like Modula-3 the only
behaviour prescribed is that it is a checked runtime error with leaves
the implementation with much more freedom. One way to solve this is to
do the rearrangements with the minimal checks to determine a bounds
violation and on detection switch to a slower version of the routine
that has the correct error behaviour but this would introduce a lot of
code bloat.

-- 
Lieven Marchand <mal@bewoner.dma.be> 
------------------------------------------------------------------------------
Few people have a talent for constructive laziness. -- Lazarus Long

Re: Idea: Array Boundary Checks on Write Access Only

[Robert I. Eachus]

In article <6me766$l4t$1@xenon.inbe.net> Lieven Marchand <mal@bewoner.dma.be> writes:

  > One of the problems in doing this with Ada is that the language spec
  > describes the exact behaviour for errors like this. You have to raise
  > the correct exception after having done all the previous effects. This
  > restricts the freedom of the compiler to rearrange checks. In
  > languages with similar semantics for arrays like Modula-3 the only
  > behaviour prescribed is that it is a checked runtime error with leaves
  > the implementation with much more freedom...

   Sounds like Ada 83, not Ada 95.  From a user point of view, 11.6 is
a lot more strict in Ada 95 about the semantics of programs which do
not raise a predefined exception (in practice, Constraint_Error) and a
lot less strict about programs which do.  The intent is that when
Constraint_Error occurs, the only thing you know in the handler is
that it was raised by code in the scope of the handler.  Basically,
all variables potentially assigned to in that scope can become
"abnormal", and references to them erroneous.

   It does mean that you need to do a lot more work if you actually
intend to recover from a particular arithmetic overflow, but unless
you wrapped every arithmetic operation in the scope in a separate
handler in Ada 83, you were in basically the same boat.

   For example:

     begin
       for I in Some_Range loop
         A(I) := B(I) + C(I);
       end loop;
     exception
       when Constraint_Error => ...;
       -- I and all elements of A should be treated as bogus.
     end;

   To find where the error occurs you need to write:

     begin
       for I in Some_Range loop
         begin
           A(I) := B(I) + C(I);
         exception
           when Constraint_Error => ...;
           -- I can be trusted
         end;    
       end loop;
     exception
       when Constraint_Error => ...;
       -- Absent a raise, A is okay here, but I is not.
     end;
--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...

Re: Idea: Array Boundary Checks on Write Access Only

[Robert Dewar]

It seems odd to have *any* runtime checks that can raise exceptions in
safety critical progams. Such programs are not supposed to have errors
that could write arrays out of bounds, and the certification and validation
process should be able to prove the absence of such errors.

Re: Idea: Array Boundary Checks on Write Access Only

[Robert Dewar]

<<> It would then also be a nice option if the compiler would be
> able to dump a list of all the checks that it still had to insert
> to give developers a clue of whether they can by intelligently
> placing a manual check at the right place make a large number
> of automatically inserted less efficient checks unnecessary.
>>


In fact the RM requires (in annex H) that a fuloly conforming compiler
have some way of informing you of runtime time checks that are inserted.

Re: Idea: Array Boundary Checks on Write Access Only

[Markus Kuhn]

Robert Dewar wrote:
> 
> It seems odd to have *any* runtime checks that can raise exceptions in
> safety critical progams. Such programs are not supposed to have errors
> that could write arrays out of bounds, and the certification and validation
> process should be able to prove the absence of such errors.

On this topic, read also the famous Ariane 5 maiden flight failure
analysis:

  http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html

The reason for the crash in the end was an unhandled Ada overflow
exception. There would have been no problem here if this piece of
navigation system control code had been compiled without exceptions.

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>

Re: Idea: Array Boundary Checks on Write Access Only

[Frank Klemm]

On 22 Jun 1998 00:44:07 -0400, Robert Dewar <dewar@merv.cs.nyu.edu> wrote:
>Markus said
>
><<The reason for the crash in the end was an unhandled Ada overflow
>exception. There would have been no problem here if this piece of
>navigation system control code had been compiled without exceptions.
>>>
>
>Indeed, and I often use this case as an example of the important fact that
>runtime checking does not necessarily improve safety, and indeed if exceptions
>can be raised, it is vital that VERY careful analysis of all exceptional
>situations take place to make sure they are handled. In the absence of
>such careful analysis, running with checks on can be much more dangerous
>than with checks off. Very often, a locally violated constraint will just
>cause a local wrong value with checks off, which may not be critical,
>especially if the wrong value is in connection with a non-critical function.
>But raising an exception can have disastrous global effects if the exception
>is not properly handled.
>
Do no check for a condition if you're not known how to handle it!

-- 
Frank Klemm

 /------\  /-----------------------------------------------------\
| eMail: || pfk@uni-jena.de | home: pfk@schnecke.offl.uni-jena.de |
| Tel:   ||                 | home: +49 (3641) 390545             |
| sMail: ||  Frank Klemm, Ziegesarstr. 1, D-07747 Jena, Germany   |
 \------/  \-----------------------------------------------------/