Similarities and differences between PCC and TAL

Both support memory safety and type safety. At least in theory, PCC supports 
a richer set of policies in a more flexible way. However, in practice, type 
safety can include many of the features that PCC claims to have.

In PCC, the security policy, the checker and the generator are three 
independent components and the checker is considered to be small and less 
prompt to errors. The proof is encoded in a logic.

In TAL, the checker includes the policy (type rules) and the proof generator 
(to find the proof), and it is considered to be a specialized proof checker. 
That makes the checker more cumbersome and complicated. TAL uses types 
directly, while PCC uses policies. The compiled source code produces an 
object file (*.o) and its associated file of types (*.fo), which is 
equivalent to the proof in PCC.

From an architectural viewpoint, PCC seems to be more desirable and 
flexible, but in practice there seems to be that the advantage is only 
theoretical.

Proof Carrying Code

PCC uses symbolic formulas and expressions as building blocks for its logic.

A list of integers or pairs is used to illustrate the main principles.

When an integer is referenced we have an odd address, in case of a pair we 
have an even address.

For instance, using the word and structured types we can define:

E:{x |  even(x) => x:ptr(int,int)}
E:int   [Used by default]

The second definition can be ignored and considered as by default.