Tag: software-safety

George Necula's proof-carrying code shifted trust toward machine-checkable evidence: untrusted code could arrive with a proof that it satisfied a receiver-defined safety policy.