Typed process in untyped contexts
(Abstract)
Michele Bugliesi
Dipartimento di Informatica,Universit`a Ca’Foscari di Venezia
joint work with
Marco Giunti
Dipartimento di Informatica,Universit`a Ca’Foscari di Venezia
1Background
The u of types to control the behavior of process in the pi-calculus is a long known and well established technique.The idea wasfirst introduced by Pierce and Sangiorgi in their minal work on the subject[9],and is best illustrated by their motivating example:
S=(νs)!d s |!s(x).print x C=d(x).x j
S is a print spooler rving requests from a private channel s that it communicates to its clients via the public channel d.C is one such client,that receives s and us it to print the job j.
While the intention of the specification is clear,reasoning on its properties is subtler. For instance,given the initial configuration S|C,can we prove that the jobs nt by C are eventually received and printed?Stated in more formal terms:is there a proof of the following equation?
S|C ?∼
=S|print j (1)
Here we take P∼=Q to mean that P and Q are behaviorally hey have the same obrvable behavior when executed in any arbitrary context.Back to our example,(1)is easily disproved by exhibiting a context that interferes with the intended protocol between S and C.Afirst example is the context C1[−]=−|d(x).!x(y).0,that initially behaves as a client,to receive s,but then steals the jobs intended for S.A cond example is the context C2[−]=−|(νs )d s ,which may succeed in transmitting to C a dead-ended channel that will never rve the purpo C expected of it.
As shown in[9],hostile contexts such as tho above can be ruled out by resorting to a system of cap
ability types to control the transmission and/or reception of values over channels bad on the posssion of corresponding type capabilities.In our example, that system allows us to protect against contexts like C1by requiring that clients be only granted write capabilities on the channel s,and by rerving read capabilities on s to the spooler.Similarly,we may build safeguards against attackers like C2by demanding that clients only have read access on d.
Work supported by EU FET-GC project‘MyThS’IST-2001-32617
say什么意思
Both the requirements are expresd formally by the typing assumption d:((T)w)r: this typing grants read-only access on d and write-only access to any name received on d,as desired.We may now refine the equation in(1)into its typed version below:
d:((T)w)r|=S|C∼=S|print j .(2) Typed equations of the form I|=P∼=Q express behavioral equivalences between pro-cess in any context that typechecks in the type environment I.Here I reprents the context’s view of the process under obrvation,given in terms of a t of typing assumptions on the names shared between the process and the context itlf.Inci-dentally,but importantly,the typing assumptions on the shared names may in general be different–in fact,more accurate–for the process than they are for the context. To illustrate,in(2),a context is only assumed to have read-ca
pabilities on d,while for the system to typecheck the name d must be known at the lower(hence more accu-rate)type((T)w)rw,so that to allow S to write and C to read.Similarly,for the system S|C to typecheck,the name s must be known at the type(T)rw including both a write-capability,granted to S,and read-capability,granted to any process that receives s:the context,instead,will only acquire s at the super-type(T)w determined by the type of the transmission channel d.
2Typed equivalences fail in untyped contexts
Given the type for d available to the context,it is not difficult to be convinced that(2) above reprents a valid equivalence,as no context that typecheks under d:((T)w)r may tell the two process apart.
Typed equivalences like the are very uful,and effective in all situations in which we have control on the contexts obrving our in all situations in which we may assume that such contexts are well-typed,hence behave according to the in-variants enforced by the typing system.
The question we address in this abstract is whether the same kind of reasoning can still be relied upon when our process are to be deployed in distributed,open envi-ronments.Stated more precily:can we implement our typed process as low-level agents to be executed in arbitrary,open networks,while at the same time prerving the typed behavioral congruences availabl
conveniencee for the source process?
One is readily convinced that no implementation with the desired properties may rely on static typing alone,as distributed and open networks do not validate any uful assumption on the trustworthiness,hence the well-typedness,of the contexts where(the low-level agents reprenting)our typed process operate.Rather than assuming that a context satisfies the constraints impod by a typing assumption,our implementations should enforce them.
The implementation schema we envision here is one in which the statically checked posssion and distribution of type capabilities in the source-level process is realized in terms of the posssion and the dynamic distribution of corresponding term-level capabilities in the implementation agents.For instance,each channel could be imple-mented by means of a pair of cryptographic keys reprenting the write and read ca-
2
pabilities.If designed carefully,and instrumented with adequate measures to protect against hostile contexts(cf.[1,3,7])this reprents a viable idea to pursue.
The problem remains,however,to make sure that the implementation prerves the desired typed equations of the source calculus:for that to be the ca,one must guarantee that for each name,the distribution of the term capabilities in the low-level agents match the corresponding type capabilities in the source level process.While this is possible for the names that are statically shared with the context,ensuring such correspondence is much harder,if at all possible,for the names that are dynamically acquired by the context.There are two fundamental difficulties:
–first,as we have obrved,the type at which the context acquires a name depends on the type of the channel over which the name is communicated;
–condly,the type of the transmission channel may vary dynamically in ways that cannot be predicted statically.
The dynamic evolution is particularly problematic in a calculus with matching becau, as noticed by Hennessy and Rathke in[8],matching makes it possible to progressively refine the type at which a name is known during the computation.This is best illustrated by the following typed labelled transition,borrowed from[8],that formalizes the effect of emitting a name on a public channel.
I r(a)↓
I a n .P
a n
加州大学圣芭芭拉−−→I n:I r(a) P
The configuration I P reprents a process P operating in a context that typecheks under I,and I r(a)↓indicates that I(hence the context)has a read capability on the name a.The meet I n:I r(a)in the resulting configuration reprents the ability of the context to“merge”its current type for n with the type determined by receiving n on a: as explained in[8],taking the meet mimics the ability of the context to match n with the names already known to it(possibly,at different types),and obtain a more informative type bad on that.The problem is that the effect of this type refinement may propagate dynamically in ways that cannot be determined statically.To illustrate,let I and P be the typing environment and the process defined as follows:
I=n:((T)w)r,a:(((T)r)r)r
P=a n |(νp:(T)rw)n p
We have I r(n)=(T)w and I r(a)=((T)r)r,and from this we compute I I n:I r(a)= a:(((T)r)r)r,n:((T)rw)r.Nocf是什么
w we e that a context that typechecks under I will ac-quire p at the type(T)w or at the type(T)rw depending on which one of the two names p and n it receivesfirst in its interactions with process P.This is reflected by the following two transition quences available from I P.
I P
(νp)n p
−−−−−→I,p:(T)w a n
a n
−−→I n:((T)r)r,p:(T)w 0
I P有么说么
a n
−−→I (νp:(T)rw)n p
(νp)n p
−−−−−→I ,p:(T)rw 0考研英文
3
Clearly,this dynamic evolution of the typing knowledge of the context is problem-atic,as a fully abstract implementation would need to tune the distribution of the term-capabilities associated with n on the types available dynamically to the context:as the example shows,this is in general impossible to achieve at compile time,by simply inspecting the structure of the source level process.
3Dynamic typing to the rescue
While the problem with the previous example is a direct conquence of the prence of matching,a more fundamental obstacle against full abstraction is in the very structure of the capability types adopted in the source calculus,and in the way that structure determines the acquisition of new capabilities on a name.As we have shown,acquiring a name,say n,at a type not only informs on how n will be ud,but also determines how other names transmitted over n will be circulated and ud in the system.The invariants are all encoded in the static type of the channel at which n is received,and clearly they will not be guaranteed if that channel is shared with an untyped context.
To make a fully abstract implementation feasible,the solution we propo here is to adopt a new typing discipline for the source calculus,bad on a combination of static and dynamic typing to control the interaction with the context.
We formalize our approach by introducing a typed variant of the(asynchronous) pi-calculus.In this calculus,named API@,the types at which the emitted values are to be received by the context are decided the output sites.This is accomplished by intro-ducing a new output construct,noted a v@T ,that relies on type coercion to enforce the delivery of v at the type T,regardless of the type of the communication channel a.A static typing system will ensure that v has indeed the type T to which it is coerced,while a mechanisms of dynamically typed synchronization guarantees that v is received only at supertypes of T,so as to guarantee the type soundness of each exchange of values.
By breaking the dependency between the types of the transmission channels and the types of the names transmitted,in API@we may safely dispen with the nested types of[9,8],and rely instead on channel types with aflat structure that only exhibits the read/write access rights associated with the channels,regardless of the types of the values they transmit.Needless to say,the resulting discipline of static typing is much loor:to compensate for that one then needs a dynamically typed operational mantics to ensure type soundness.
What is more interesting and relevant for our prent concerns is that the new typing discipline makes it possible to recover fully abstract implementa-tions for which the typed congruences of the source calculus are prerved even in the prence of untyped,and potentially hostile contexts.We give a brief overview of how that can be accomplished in Section6.Before that,we introduce the source calculus formally,and look at the conquences of the new typing discipline on the ability to reason about process behavior.
4
4A pi-calculus with dynamic typing
API@is a typed dialect of the asynchronous pi-calculus[5].The choice of an asyn-chronous calculus is only meant to ea the implementation in[7],and has no effect or conquence on our prent development.
We presuppo countable ts of names and variables,ranged over by a−n and x,y,...respectively.We u bv to denote basic values,and u,v to range collectively over names,variables and basic values whenever the distinction does not matter.The structure of process is defined by the following productions:
P,Q,...::=0|P|Q|(νn:A)P|!P pi-calculus
|[u=v]P;Q matching
|u ˜v@˜A type-coerced output
|u(˜x@˜A).P typed input
We u˜u and˜A to note(possibly empty)tuples of values and types,respectively,and the notation˜v@˜A as a shorthand for v1@A1,...,v n@A n.As in companion calculi,the typ-ing system rules out meaningless terms,like bv(x).P,that u basic values in positions where names are expected.
The reading of the process forms is standard,with the exception of the constructs for input/output.As we anticipated,u ˜v@˜A reprents the output of the values˜v at the types˜A:the rules of the operational mantics will ensure that outputs at this type only synchronizes with input prefixes expecting values at types higher than(or equal to)˜A.
The types of API@include types for basic values,a top type and capability types for names.As promid in Section3,the channel types we u have theflat structure de-fined in Table1,that informs
on the access rights associated with the channel:read(r), write(w)or both(rw).The subtyping relation,also in Table1,is the preorder that satis-fies the expected relationship over capability types,and admits a partial meet operator defined by the two claus r w=rw,A =A for all A,and undefined elwhere.
4.1Typing System
Most of the typing rules are standard and lf explained,with the two exceptions we discuss next.The typing of matching is inherited,unchanged,from[8]:as in that ca,it requires a few preliminary definitions to formalize the structure of typing environments. We build type environments,notedΓ,by using the operator :Γ u:A=Γ,u:A if u∈dom(Γ),otherwiΓ u:A=Γ whereΓ differs fromΓonly at u,since the capability of this identifier is extended to beΓ(u) A(ifΓ(u) A is undefined,then so is Γ u:A).We u the notationΓ (v1,...,v n):(A1,...,A n) Γ v1:A1 ... v n:A n, and in ca dom(Γ)∩dom(Γ )=/0,we writeΓ,Γ to indicate the type environment containing all mappings inΓand inΓ .Subtyping is extended to type environments as expected.We writeΓ<:Γ ifΓ(u)<:Γ (u)for all u∈dom(Γ).If the type environment Γat n has a type of the form r or rw thenΓr(n)is defined(written asΓr(n)↓)and we haveΓr(n)=A.Similarly for the dual ca of write capabilities.
5
Table1The typing system
Types
A,B,...::=rw|r|w capabilities
|B basic values
| top Subtyping
rw<:r rw<:w A<: Typing Rules
(T-Pro)(T-Tuple)
Γ(u)<:A Γ u:Aberzerk
Γ v i:A i∀i∈1..n
Γ (v1,...,v n):(A1,...,A n)
(T-New)(T-Par)(T-Repl)(T-Nil)
Γ,n:rw P Γ (νn)P
Γ PΓ Q
Γ P|Q
Γ P
Γ !PΓ 0
(T-Match)
embedmovie
Γ QΓ(u)=AΓ(v)=BΓ u:B v:A P
Γ [u=v]P;Q
(T-Out@)(T-In@)
Γw(u)↓Γ ˜v:˜B
Γ u ˜v@˜B
Γr(u)↓Γ,˜x:˜A P
Γ u(˜x@˜A).P
三月英文The typing of input/output is characteristic of our prent calculus,and is a direct conquence of the structure of the channel types.In particular,notice that the rules(T-
OUT)and(T-IN)do not expect/impo any relationship between the type of the channel u and the types associated with the values transmitted(in(T-OUT))or expected(in(T-
IN)).The only constraint,at the output sites,is that the types at which the emitted values are coerced must be valid.As we mentioned earlier,this rather loo form of static typing is complemented by dynamic type checks to be performed upon synchronization.
4.2Operational Semantics
The dynamics of the calculus is defined by means of a labelled transition system built around the following actions:
Actionsα::=τ|u(˜v@˜B)|(˜c:˜C)u ˜v@˜B
冷静的英文
Most of the transitions,in Table2,are standard.The output action(˜c:˜C)u ˜v@˜B carries a type tag along with the output value:it reprents the output of(a tuple,possibly including fresh)values˜v at the types˜B.Dually,the input action u(˜v@˜B)reprents
6
