Lambda the Ultimate

inactiveTopic A Language Based-Approach to Security
started 12/6/2000; 7:41:10 PM - last post 12/7/2000; 7:01:30 AM
Chris Rathman - A Language Based-Approach to Security  blueArrow
12/6/2000; 7:41:10 PM (reads: 1094, responses: 2)
A Language Based-Approach to Security
The paper explains an approach to using languages and compilers to help enforce security policies. The idea is to have the compiler verify the type safety of the compiled program. The result would be to output Proof Carrying Code (PCC) with a digital signature that verifies that the code doesn't do anything nasty. The burden of security is put on the producer of the software and away from the consumer (currently enforced in a Virtual Machine such as JVM).

Interesting concept that goes well beyond the concept of digital signatures used by Active-X. The compiler guarantees that the progam does not violate mapped out security policies. The digital signature guarantees the code has been stamped by the compiler. In-line reference monitors do the rest of the chores.
Posted to "" by Chris Rathman on 12/6/00; 7:42:16 PM

Chris Rathman - Re: A Language Based-Approach to Security  blueArrow
12/6/2000; 7:50:56 PM (reads: 1120, responses: 0)
Was getting a little to wordy on the front page, but I did want to make one point. The biggest problem I see with the PCC concept is one of liability of the compiler vendor. With PCC, the statement is being made that the compiler is giving a "Proof" that the code will not do anything nasty.

It asks us to basically place our trust in those that wrote the compiler. If a commercial vendor was to issue proof for some code, there'd have to be a lot of legalese statements about how they make no guarantees about the code - which seems to be counterintuitive to the concept of "Proof".

Of course, we have a similar situation with the client scheme used by the Java Virtual Machine. The difference being that any errant code is not code proofed by the JVM - or at least not presenting any concept of proof.

AndrewM - Re: A Language Based-Approach to Security  blueArrow
12/7/2000; 7:01:30 AM (reads: 1101, responses: 0)
This isn't entirely accurate. In fact, in the PCC scheme the compiler is in fact completely untrusted. The client does not have to trust the foreign compiler. Instead, the trusted computing base consists only of something like the safety policy and a proof-checker. For both of these, verification is easier, because they are much smaller programs than a compiler.

So I would say the issue of liability still arises, but it is not the compiler vendor who would ever be liable, but instead perhaps the company that wrote the checking software. However, as I understand it, the hope is that such software is simple enough that it is actually possible to ensure that it is correct.

There is more information on PCC here.