Static analyses allow dangerous code to be rejected before it runs. The distinct security concerns of code providers and end users necessitate that analysis be performed, or at least confirmed, during deployment rather than development; examples of this approach include bytecode verification and proof-carrying code. The situation is more complex in multi-party distributed systems, in which the multiple web services deploying code may have their own competing interests. Applying static analysis techniques to such systems requires the ability to identify the codebase running at a remote location and to dynamically determine the static properties of a codebase associated with an identity. In this paper, we provide formal foundations for these requirements. Rather than craft special-purpose combinatory to address these specific concerns, we define a reflective, higher-order applied pi calculus and apply it. We treat process abstractions as serialized program files, and thus permit the direct observation of process syntax. This leads to a semantics quite different from that of higher-order pi or applied pi.
展开▼
