|
Abstract:
Acute is an extension of an OCaml core, which provides mechanisms to support distributed development, deployment and execution of separately-built programs. The language, amongst other constructs, supports computing of distributed values with procedures for (un)marshal, which permits cooperating programs to send and receive values along un-typed communication channels. Acute implements marshal and unmarshal primitives that are type-safe and abstraction-safe, in a trusted setting. Because of this, type errors can not occur when a program does unmarshal of a received value, provided that all communications are trusted. In this talk we present an extension of the Acute language which allow us to verify invariants of certain abstract types at unmarshal time. This extension increases robustness of unmarshalled values in the presence of active adversaries. |