Re: Idea: Array Boundary Checks on Write Access Only

[nobody@REPLAY.COM (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/