Provably Correct Crypto?

At 4:15 PM 8/1/95, Ray Cromwell wrote:

>  That's a neat metaphor, but it doesn't always apply. It shouldn't
>apply to algorithms which are primitive recursive. Elementary
>algorithms like multiprecision add, sub, multiply, divide, modmult,
>and modexp (the basis of public key encryption) are all provably
>correct and all terminate. (the basis is polynomial operators over a
>ring) It is possible to verify the implementation (assuming the
>correctness of the compiler). Now there could be a "factoring"
>trapdoor in RSA, but that's a trapdoor not in the implementation of
>PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably
                                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>provably correct.  To guard against trapdoors in PGP, you should
 ^^^^^^^^^^^^^^^^^
>verify the correctness of the PRNG, Key Generator, and that no private
>key bits or session key bits are leaked. I would suspect this could be
>difficult, but approximations could be determined to within a high
>degree of confidence.

This doesn't seem likely. I mean, doesn't "RSA-in-4-lines-of-Perl" *of
necessity* make use of external library/utility functions? Such as the "dc"
math routines for the PRNG? Part of its compactness is that it makes use of
available libraries.

Anything that "reaches out" to external libraries or utilities would then
have the vulnerabilities of _those_ libraries and utilities, which may or
may not be provably correct themselves. (And the issue of any PRNG being
probably correct or not is of course an interesting, and deep, question.)

I do think the issues of modular design and provable correctness--or
approximations to it--are interesting ones.

--Tim May

..........................................................................
Timothy C. May         | Crypto Anarchy: encryption, digital money,
tcmay@sensemedia.net   | anonymous networks, digital pseudonyms, zero
408-728-0152           | knowledge, reputations, information markets,
Corralitos, CA         | black markets, collapse of governments.
Higher Power: 2^756839 | Public Key: PGP and MailSafe available.
"National borders are just speed bumps on the information superhighway."

Hello Ray Cromwell <rjc@clark.net>, patl@lcs.mit.edu
  and tcmay@sensemedia.net (Timothy C. May)
  and cypherpunks@toad.com

> At 4:15 PM 8/1/95, Ray Cromwell wrote:
...
> >PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably
>                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> >provably correct.  To guard against trapdoors in PGP, you should
>  ^^^^^^^^^^^^^^^^^
...
[emphasis tcmay]

To which tcmay responded:

> This doesn't seem likely. I mean, doesn't "RSA-in-4-lines-of-Perl" *of
> necessity* make use of external library/utility functions? Such as the "dc"
> math routines for the PRNG? Part of its compactness is that it makes use of
> available libraries.
...

AFAIK (my 4 lines might differ from yours), there is no PRNG in the
4 lines of perl. The key is supplied as a parameter, and no guidance
to its generation is given in the implementation.

You are right about the dc, but it only uses that for modular exponentiation,
which is a lot easier to prove correct than PRNG.
Which is not to say that it *has* been proven.


I guess that makes me a nit-picker...

Jiri
--
If you want an answer, please mail to <jirib@cs.monash.edu.au>.
On sweeney, I may delete without reading!
PGP 463A14D5 (but it's at home so it'll take a day or two)

...
> >PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably
>                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> >provably correct.  To guard against trapdoors in PGP, you should
>  ^^^^^^^^^^^^^^^^^
> >verify the correctness of the PRNG, Key Generator, and that no private
...
> This doesn't seem likely. I mean, doesn't "RSA-in-4-lines-of-Perl" *of
> necessity* make use of external library/utility functions? Such as the "dc"
> math routines for the PRNG? Part of its compactness is that it makes use of
> available libraries.

This issue is an interesting one and one worthy of being addressed. 
There are a couple of concerns here (I approximately quote from a
submitted paper on the secure W3 server with quotation marks):

Concern 1:
	"The secure (program) is designed in such a way that we can
	demonstrate (subject to the propriety of compilers, operating
	system functions, and other things in the environment) that once
	the daemon is started, only the desired affects result." 

Concern 2:
	The environment has an insecurity specific to the secure
	program used as a means of subverting the function of the
	secure program.

I pretty much believe that Concern 1 should be addressed by all programs
that claim to be secure.  That is, subject to the rest of the world woking
right, the secure program works right.

I believe that concern 2 should be addressed by all programs that claim
to be secure in a particular environment.  That is, beyond being secure
assuming the environment is secure, we might want to eliminate the
assumption about the environment by showing it to be justified.  In
terms of attacking systems, it is necessaary to subvert many different
environments for this issue to be important for widespread use of PGP,
or at least to subvert several of the more common environments (such as
what the Thompson c compiler mentioned in his Turing award talk did).

> Anything that "reaches out" to external libraries or utilities would then
> have the vulnerabilities of _those_ libraries and utilities, which may or
> may not be provably correct themselves. (And the issue of any PRNG being
> probably correct or not is of course an interesting, and deep, question.)
> 
> I do think the issues of modular design and provable correctness--or
> approximations to it--are interesting ones.

I think that this issue can generally be addressed by a divide and
conquer strategy.  Prove that the called routines are correct and
confined under all possible parameters, do the same for the calling
routines, do the same for the interaction between them, and I think you
have it.  This is pretty easy for one or two routines, but when you take
the OS into account, the C compiler into account, the program itself
into account, and the external environment into account, you run into
some serious limitations.  For example, you may (in some cases) have to
show that under all possible sequences of interrupt timings and stack
conditions, the system operates correctly (which almost none currently
do).  Unless you design with this sort of thing in mind, it's very hard
to demonstrate these properties even for limited subproblems. 

-- 
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236

Hmm. Instead of "vetting" the PGP PRNG code, as Dr. Cohen has been
trying to tell me in private email is several programmer- years worth
of work perhaps I should just write my own version of the PRNG using
the algorithm as defined in whitepapernumberwhatever.

If there are artificial "bugs" to throw off the PRNG currently in the
PGP MIT code, they ought to simply not work right with the code I
write independently and therefore cause a crash or something.

Or perhaps just rewrite the program to use plain arrays instead of
pointers. ;-)

Phil

Phil writes:
> Or perhaps just rewrite the program to use plain arrays instead of
> pointers. ;-)

How about Java-PGP ?  ;)

-Futplex

The shadowy figure took form and announced "I am Dr. Frederick B. Cohen and I s
ay ...

[ lots of purely subjective arguments that frequent alt.security.pgp ]

Frederick can you please tell me why I should belive thttpd is secure.
I don't accept the ability to compile it myself as evidence and I
don't accept a summary of that source written in english prose on the
basis that it has no hard link what so ever to the source.  It was
also written by the authors of thttpd.

You should find this argument hauntingly familiar.

You state that crypto should be poved correct and suggest a technique
otherwise known as formal specification.  I agree, pgp should have
been written in Z-specs.  If you take a course in formal specification
you will soon see the intractability of the technique wrt large
systems.

I'm sorry, the english prose your team writes holds no extra formal
credibility over trust.  It demonstrates more study - but has not
proven security.

If you want prople on this list to repeat after you "I cannot be
certain there is no compromising bugs or backdoors in X" Then I will
go out on a limb and say everyone here will agree if system X is
sufficiently large.

p.s X = thttpd

--
                                          <URL:http://www.comp.vuw.ac.nz/~matt>
                 |~    |~
             |~ o|    o|
       ('<  o| 
      ,',)   
     ''<<    
     ---""---

...
> Frederick can you please tell me why I should belive thttpd is secure.
> I don't accept the ability to compile it myself as evidence and I
> don't accept a summary of that source written in english prose on the
> basis that it has no hard link what so ever to the source.  It was
> also written by the authors of thttpd.

The reason to believe that thttpd fulfills the claims it makes is
provided in some detail in the white paper on our server (see what's new
under http://all.net).  A slightly more detailed version has been
submitted for a journal article, and hopefully will appear in a year or
two.

Certainly compiling it yourself would not in any way help you assert its
security, however it would help you assure that the compiled version (which
we don't provide on-line) is not an altered executable.

I would detail the full set of claims here, but this is not the proper
forum for general security issues.  Of course if there is popular
support, I would be glad to... Instead, I will briefly outline it here:

The basic reason that thttpd can be verified to fulfill the claimed
security properties relate to some well thought-of and mathemtically
proven theories about information flow.  Specifically:

	we have shown that information coming from the client cannot
	flow to the server except in its effects of sending the requested
	file (if it exists, is properly owned, and is properly protected
	for access by remote users) and logging the request in the log
	file generated by the program.  If no information can flow from
	the client to the server data, the client cannot cause
	corruption of the server (subject to various details not
	included here).

	we have shown that the server is a limited function program (i.e.,
	does not have Turing capability), and that therefore no general
	purpose operations can be performed as a result of any external input.

	we have shown that the variables and structures are confined so
	as to have no unspecified side effects, and that therefore there
	are no effects other than those stated in the description of the
	program.

	we have also shown some other stuf you might be interested in.

The next logical question is why those are worthwhile things to show,
and I won't get into these details here without further prompting.

> You should find this argument hauntingly familiar.

I welcome your questions about "why" as I always do.  I think that
this is a very important question and one worth following up.

> You state that crypto should be poved correct and suggest a technique
> otherwise known as formal specification.  I agree, pgp should have
> been written in Z-specs.  If you take a course in formal specification
> you will soon see the intractability of the technique wrt large
> systems.

I didn't say that.  Perhaps you should review what I said before
characterizing it.

> I'm sorry, the english prose your team writes holds no extra formal
> credibility over trust.  It demonstrates more study - but has not
> proven security.

I have shown (not yet proven) certain things.  A graduate student is now
working on trying to prove the various properties I believe to be of
interest in an automatic theorum prover he is working on.  I believe
that these things are worth showing (and proving), but you may certainly
feel free to disagree with these contentions.

> If you want prople on this list to repeat after you "I cannot be
> certain there is no compromising bugs or backdoors in X" Then I will
> go out on a limb and say everyone here will agree if system X is
> sufficiently large.

I don't believe I ever asked anyone on this list to repeat anything. 
All I did was ask questions and respond to responses to my questions.

-- 
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236

On Tue, 1 Aug 1995, Dr. Frederick B. Cohen was alleged to have blathered:

> Tim May mused:

> > Anything that "reaches out" to external libraries or utilities would then
> > have the vulnerabilities of _those_ libraries and utilities, which may or
> > may not be provably correct themselves. (And the issue of any PRNG being
> > probably correct or not is of course an interesting, and deep, question.)
> > 
> > I do think the issues of modular design and provable correctness--or
> > approximations to it--are interesting ones.
> 
> I think that this issue can generally be addressed by a divide and
> conquer strategy.  Prove that the called routines are correct and
> confined under all possible parameters, do the same for the calling
> routines, do the same for the interaction between them, and I think you
> have it.  This is pretty easy for one or two routines, but when you take
> the OS into account, the C compiler into account, the program itself
> into account, and the external environment into account, you run into
> some serious limitations.  For example, you may (in some cases) have to
> show that under all possible sequences of interrupt timings and stack
> conditions, the system operates correctly (which almost none currently
> do).  Unless you design with this sort of thing in mind, it's very hard
> to demonstrate these properties even for limited subproblems. 
> 

After all your griping over PGP, you spout this?  Have you ever heard of 
Godel's theorem?  I have a phrase for people who peddle their mark of 
approval that a given large program will work: "Snake oil salesman".  In 
the messages which you have scrawled between this and the last on my 
system when I caught up this evening, you have demonstrated the 
fraudulent nature of your business by first claiming that certain 
propositions were "demonstrated", then stating that a graduate student 
was working on "proving" them.

I repeat: Snake Oil Salesman

<PLONK>

> > I think that this issue can generally be addressed by a divide and
> > conquer strategy.  Prove that the called routines are correct and
> > confined under all possible parameters, do the same for the calling
> > routines, do the same for the interaction between them, and I think you
> > have it.  This is pretty easy for one or two routines, but when you take
> > the OS into account, the C compiler into account, the program itself
> > into account, and the external environment into account, you run into
> > some serious limitations.  For example, you may (in some cases) have to
> > show that under all possible sequences of interrupt timings and stack
> > conditions, the system operates correctly (which almost none currently
> > do).  Unless you design with this sort of thing in mind, it's very hard
> > to demonstrate these properties even for limited subproblems. 
> > 
> 
> After all your griping over PGP, you spout this?  Have you ever heard of 
> Godel's theorem?

I think so.  From my understanding, it basically says that, in the
general system, you can write a legitimate expression that expresses its
own illegitimacy, or in other words that the general system is
incomplete "...in the sense that it fails to provide a proof for every
formula which is true under the interpretation..." (quoted from
"Introduction to Metamathematics" by S.C.  Kleene 1952,...,1980)

But I think you misinterpret this.  This does not mean that no program
can be proven to meet any properties.  It means that, among other
things, there are an infinite number of infinite expressions that cannot
be proven, but it does not mean that a finite expression (e.g., a
typical modern program) cannot be proven to meet all sorts of
properties.

In particular, for certain classes of programs, proofs about the flow of
information are not exceedingly complex to establish.  In general (as
was proven in the early 1980s), tracking information flow in a program
is NP-complete, however, in a program designed to limit information flow
this can be very straight forward (in fact I think it may be linear time
and space).  By proving that information doesn't flow from place to
place, we can essentially prove that information in one place does not
affect information in another place (by information thoeory), and
therefore greatly reduce the complexity of demonstrating various things
of particular interest to information security - to wit - that item A
doesn't corrupt item B, and that information in item A is not leaked to
item B.

>  I have a phrase for people who peddle their mark of 
> approval that a given large program will work: "Snake oil salesman".

In the case of the http daemon, it is a relatively small program of less
than 80 lines designed to be secure in various ways.  In the case of PGP
it is a relatively larger program that it not designed to be secure.

>  In 
> the messages which you have scrawled between this and the last on my 
> system when I caught up this evening, you have demonstrated the 
> fraudulent nature of your business by first claiming that certain 
> propositions were "demonstrated", then stating that a graduate student 
> was working on "proving" them.

How is it fraudulent to accurately state the facts?

> I repeat: Snake Oil Salesman

-- 
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236

[Tim responds to my note on "provably correct implementation"}

> 
> Anything that "reaches out" to external libraries or utilities would then
> have the vulnerabilities of _those_ libraries and utilities, which may or
> may not be provably correct themselves. (And the issue of any PRNG being
> probably correct or not is of course an interesting, and deep, question.)
> 

  What I meant by my message is in some circumstances, an implementation
can be proven correct (i.e. to do what it says it does correctly) What
I mean by implementation is the source at the highest level, not the
module dependencies which are abstractly disconnected from the application.
(e.g. if a multiprecision math library that comes with the operating
system is used by PGP, the source to PGP could be said to be "trapdoor free"
even if the math library has an NSA monitoring function built into it)

 Each layer of course relies on the correctness of the layer beneath it, much
like a theorem proof relies on the proof of the statements that makes it
up. Thus, RSA-in-4-lines can be observed to be a correct implementation
of RSA without any trapdoors (like secretly storing or leaking private
key bits) at the level of its source code. Of course, the Perl interpreter
itself would have to be proven correct, but we assume that no RSA trap
doors have been put into perl because perl was available long before
PGP and RSA-in-4-lines perl and is widely distributed. The probability
of a trapdoor in perl is small.


The hierarchy looks like this:

RSA-in-4-lines :: DEPENDS_ON_CORRECTNESS_OF { Perl, DC, RSA_Algorithms }

Perl :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, Perl_Algorithms }
DC :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, DC_Algorithms }

C :: DEPENDS_ON_CORRECTNESS_OF { C_compiler } 
C_compiler :: DEPENDS_ON_CORRECTNESS_OF { Assembler }
Assembler :: DEPENDS_ON_CORRECTNESS_OF { instruction_set }
instruction_set :: DEPENDS_ON_CORRECTNESS_OF { hardware }

Now even if it were possible to prove the correctness of all those layers
(which I find doubtful. Some kind of Goedel/Turing limitation is going to turn
up somewhere), what if the 'hardware' isn't correct. (e.g. Pentium bug)
There could be a one-in-a-zillion bug that randomly leaks keybits. 

IMHO, there's no sense in worrying about stuff like this. If your data
is so valuable that you need absolute theoretical security, use a 
one-time-pad with a simple redundant provably secure device
(also shielded from TEMPEST attacks), and have the thing implanted
in your skull. ;-)


-Ray