Thomas Jensen

Florent Kirchner

David Pichardie

Secure the Clones * Static Enforcement of Policies for Secure Object Copying

Exchanging mutable data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker. Consequently, secure programming guidelines for Java stress the importance of using defensive copying before accepting or handing out references to an internal mutable object. However, implementation of a copy method (like clone()) is entirely left to the programmer. It may not provide a sufficiently deep copy of an object and is subject to overriding by a malicious sub-class. Currently no language-based mechanism supports secure object cloning. This paper proposes a type-based annotation system for defining modular copy policies for class-based object-oriented programs. A copy policy specifies the maximally allowed sharing between an object and its clone. We present a static enforcement mechanism that will guarantee that all classes fulfill their copy policy, even in the presence of overriding of copy methods, and establish the semantic correctness of the overall approach in Coq. The mechanism has been implemented and experimentally evaluated on clone methods from several Java libraries.

Introduction

Exchanging data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker. Consequently, secure programming guidelines for Java such as those proposed by Sun [START_REF] Develper | Secure Coding Guidelines for the Java Programming Language, version 3.0[END_REF] and CERT [START_REF]The CERT Sun Microsystems Secure Coding Standard for Java[END_REF] stress the importance of using defensive copying or cloning before accepting or handing out references to an internal mutable object. There are two aspects of the problem:

1. If the result of a method is a reference to an internal mutable object, then the receiving code may modify the internal state. Therefore, it is recommended to make copies of mutable objects that are returned as results, unless the intention is to share state. 2. If an argument to a method is a reference to an object coming from hostile code, a local copy of the object should be created. Otherwise, the hostile code may be able to modify the internal state of the object.

A common way for a class to provide facilities for copying objects is to implement a clone() method that overrides the cloning method provided by java.lang.Object. The following code snippet, taken from Sun's Secure Coding Guidelines for Java, demonstrates how a date object is cloned before being returned to a caller: However, relying on calling a polymorphic clone method to ensure secure copying of objects may prove insufficient, for two reasons. First, the implementation of the clone() method is entirely left to the programmer and there is no way to enforce that an untrusted implementation provides a sufficiently deep copy of the object. It is free to leave references to parts of the original object being copied in the new object. Second, even if the current clone() method works properly, sub-classes may override the clone() method and replace it with a method that does not create a sufficiently deep clone. For the above example to behave correctly, an additional class invariant is required, ensuring that the date field always contains an object that is of class Date and not one of its sub-classes. To quote from the CERT guidelines for secure Java programming: "Do not carry out defensive copying using the clone() method in constructors, when the (non-system) class can be subclassed by untrusted code. This will limit the malicious code from returning a crafted object when the object's clone() method is invoked." Clearly, we are faced with a situation where basic object-oriented software engineering principles (sub-classing and overriding) are at odds with security concerns. To reconcile these two aspects in a manner that provides semantically well-founded guarantees of the resulting code, this paper proposes a formalism for defining cloning policies by annotating classes and specific copy methods, and a static enforcement mechanism that will guarantee that all classes of an application adhere to the copy policy. We do not enforce that a copy method will always return a target object that is functionally equivalent to its source. Rather, we ensure non-sharing constraints between source and targets, expressed through a copy policy, as this is the security-critical part of a copy method in a defensive copying scenario.

Cloning of Objects

For objects in Java to be cloneable, their class must implement the empty interface Cloneable. A default clone method is provided by the class Object: when invoked on an object of a class, Object.clone will create a new object of that class and copy the content of each field of the original object into the new object. The object and its clone share all sub-structures of the object; such a copy is called shallow.

It is common for cloneable classes to override the default clone method and provide their own implementation. For a generic List class, this could be done as follows: Notice that this cloning method performs a shallow copy of the list, duplicating the spine but sharing all the elements between the list and its clone. Because this amount of sharing may not be desirable (for the reasons mentioned above), the programmer is free to implement other versions of clone(). For example, another way of cloning a list is by copying both the list spine and its elements 1 , creating what is known as a deep copy. A general programming pattern for methods that clone objects works by first creating a shallow copy of the object by calling the super.clone() method, and then modifying certain fields to reference new copies of the original content. This is illustrated in the following snippet, taken from the class LinkedList in Fig. 8: There are two observations to be made about the analysis of such methods. First, an analysis that tracks the depth of the clone being returned will have to be flow-sensitive, as the method starts out with a shallow copy that is gradually being made deeper. This makes the analysis more costly. Second, there is no need to track precisely modifications made to parts of the memory that are not local to the clone method, as clone methods are primarily concerned with manipulating memory that they allocate themselves. This will have a strong impact on the design choices of our analysis.

Copy Policies

The first contribution of the paper is a proposal for a set of semantically well-defined program annotations, whose purpose is to enable the expression of policies for secure copying of objects. Introducing a copy policy language enables class developers to state explicitly the intended behavior of copy methods. In the basic form of the copy policy formalism, fields of classes are annotated with @Shallow and @Deep. Intuitively, the annotation @Shallow indicates that the field is referencing an object, parts of which may be referenced from elsewhere. The annotation @Deep(X) on a field f means that a) the object referenced by this field f cannot itself be referenced from elsewhere, and b) the field f is copied according to the copy policy identified by X. Here, X is either the name of a specific policy or if omitted, it designates the default policy of the class of the field. For example, the following annotations: class List { @Shallow V value; @Deep List next; ...} specifies a default policy for the class List where the next field points to a list object that also respects the default copy policy for lists. Any method in the List class, labelled with the @Copy annotation, is meant to respect this default policy.

In addition it is possible to define other copy policies and annotate specific copy methods (identified by the annotation @Copy(...)) with the name of these policies. For example, the annotation2 DL: { @Deep V value; @Deep(DL) List next;}; @Copy(DL) List<V> deepClone() { return new List((V) value.clone(), (next==null ? null : next.deepClone())); } can be used to specify a list-copying method that also ensures that the value fields of a list of objects are copied according to the copy policy of their class (which is a stronger policy than that imposed by the annotations of the class List). We give a formal definition of the policy annotation language in Section 2.

The annotations are meant to ensure a certain degree of non-sharing between the original object being copied and its clone. We want to state explicitly that the parts of the clone that can be accessed via fields marked @Deep are unaccessible from any part of the heap that was accessible before the call to clone(). To make this intention precise, we provide a formal semantics of a simple programming language extended with policy annotations and define what it means for a program to respect a policy (Section 2.2).

Enforcement

The second major contribution of this work is to make the developer's intent, expressed by copy policies, statically enforceable using a type system. We formalize this enforcement mechanism by giving an interpretation of the policy language in which annotations are translated into graph-shaped type structures. For example, the annotations of the List class defined above will be translated into the graph that is depicted to the right in Fig. 1 (res is the name given to the result of the copy method). The left part shows the concrete heap structure.

Unlike general purpose shape analysis, we take into account the programming methodologies and practice for copy methods, and design a type system specifically tailored to the enforcement of copy policies. This means that the underlying analysis must be able to track precisely all modifications to objects that the copy method allocates itself (directly or indirectly) in a flow-sensitive manner. Conversely, as copy methods should not modify non-local objects, the analysis will be designed to be more approximate when tracking objects external to the method under analysis, and the type system will accordingly refuse methods that attempt such non-local modifications. As a further design choice, the annotations are required to be verifiable modularly on a class-by-class basis without having to perform an analysis of the entire code base, and at a reasonable cost. As depicted in Fig. 1, concrete memory cells are either abstracted as a) ⊤ out when they are not allocated in the copy method itself (or its callee); b) ⊤ when they are just marked as maybe-shared; and c) circle nodes of a deterministic graph when they are locally allocated. A single circle furthermore expresses a singleton concretization. In this example, the abstract heap representation matches the graph interpretation of annotations, which means that the instruction set that produced this heap state satisfies the specified copy policy.

Technically, the intra-procedural component of our analysis corresponds to heap shape analysis with the particular type of graphs that we have defined. Operations involving non-local parts of the heap are rapidly discarded. Inter-procedural analysis uses the signatures of copy methods provided by the programmer. Inheritance is dealt with by stipulating that inherited fields retain their "shallow/deep" annotations. Redefinition of a method must respect the same copy policy and other copy methods can be added to a sub-class. The detailed definition of the analysis, presented as a set of type inference rules, is given in Section 3. The formalism is developed for a small, imperative language extended with basic, class-based object-oriented features for object allocation, field access and assignment, and method invocation. A program is a collection of classes, organized into a treestructured class hierarchy via the extends relation. A class consists of a series of copy method declarations with each its own policy X, its name m, its formal parameter x and commands c to execute. A sub-class inherits the copy methods of its super-class and can re-define a copy method defined in one of its super-classes. We only consider copy methods. Private methods (or static methods of the current class) are inlined by the type checker. Other method calls (to virtual methods) are modeled by a special instruction x :=?(y) that assigns an arbitrary value to x and possibly modifies all heap cells reachable from y (except itself). The other commands are standard. The copy method call x :=m cn:X (y) is a virtual call. The method to be called is the copy method of name m defined or inherited by the (dynamic) class of the object stored in variable y. The subscript annotation cn:X is used as a static constraint. It is supposed that the type of y is guaranteed to be a sub-class of class cn and that cn defines a method m with a copy policy X. This is ensured by standard bytecode verification and method resolution.

Language and Copy Policies

We suppose given a set of policy identifiers Policy id , ranged over by X. A copy policy declaration has the form X : {τ } where X is the identifier of the policy signature and τ is a policy. The policy τ consists of a set of field annotations (X, f ) ; . . . where f is a deep field that should reference an object which can only be accessed via the returned pointer of the copy method and which respects the copy policy identified by X. The use of policy identifiers makes it possible to write recursive definitions of copy policies, necessary for describing copy properties of recursive structures. Any other field is implicitly shallow, meaning that no copy properties are guaranteed for the object referenced by the field. No further copy properties are given for the sub-structure starting at shallow fields. For instance, the default copy policy of the class List presented in Sec. 1.2 writes: {(List.default, next)}.

We assume that for a given program, all copy policies have been grouped together in a finite map Π p : Policy id → Policy. In the rest of the paper, we assume this map is complete, i.e. each policy name X that appears in an annotation is bound to a unique policy in the program p.

The semantic model of the language defined here is store-based:

l ∈ Loc v ∈ Val = Loc ∪ {⋄} ρ ∈ Env = Var → Val o ∈ Object = Field → Val h ∈ Heap = Loc ⇀fin (Classid × Object) ρ, h, A ∈ State = Env × Heap × P(Loc)
A program state consists of an environment ρ of local variables, a store h of locations mapping 3 to objects in a heap and a set A of locally allocated locations in the current method or one of its callees. This last component does not influence the semantic transitions: it is necessary to express the type system interpretation exposed in Sec. 3, but is not used in the final soundness theorem. Each object is modeled in turn as a finite function from field names to values (references or the specific ⋄ reference for null values). We do not deal with base values such as integers because their immutable values are irrelevant here.

The operational semantics of the language is defined (Fig. 3) by the evaluation relation between configurations Comm × State and resulting states State. The set of

(x :=y, ρ, h, A ) ρ[x → ρ(y)], h, A (x :=null, ρ, h, A ) ρ[x → ⋄], h, A ρ(y) ∈ dom(h) (x :=y.f , ρ, h, A ) ρ[x → h(ρ(y), f )], h, A ρ(x) ∈ dom(h) (x .f :=y, ρ, h, A ) ρ, h[(ρ(x), f ) → ρ(y)], A l ∈ dom(h) (x := new cn, ρ, h, A ) ρ[x → l], h[l → (cn, o⋄)], A ∪ {l} (return x , ρ, h, A ) ρ[ret → ρ(x)], h, A h(ρ(y)) = (cny, ) lookup(cny, m) = Copy(X ′ ) m(a):=c cny cn (c, ρ⋄[a → ρ(y)], h, ∅ ) ρ ′ , h ′ , A ′ (x :=m cn:X (y), ρ, h, A ) ρ[x → ρ ′ (ret)], h ′ , A ∪ A ′ dom(h) ⊆ dom(h ′ ) ∀l ∈ dom(h) \ Reach h (ρ(y)), h(l) = h ′ (l) ∀l ∈ dom(h) \ Reach h (ρ(y)), ∀l ′ , l ∈ Reach h ′ (l ′ ) ⇒ l ′ ∈ dom(h) \ Reach h (ρ(y)) v ∈ {⋄} + Reach h (ρ(y)) ∪ (dom(h ′ ) \ dom(h)) (x :=?(y), ρ, h, A ) ρ[x → v], h ′ , A\Reach + h (ρ(y)) (c1, ρ, h, A ) ρ1, h1, A1 (c2, ρ1, h1, A1 ) ρ2, h2, A2 (c1; c2, ρ, h, A ) ρ2, h2, A2 (c1, ρ, h, A ) ρ1, h1, A1 (if ( * ) then c1 else c2 fi, ρ, h, A ) ρ1, h1, A1 (c2, ρ, h, A ) ρ2, h2, A2 (if ( * ) then c1 else c2 fi, ρ, h, A ) ρ2, h2, A2 (while ( * ) do c done, ρ, h, A ) ρ, h, A (c; while ( * ) do c done, ρ, h, A ) ρ ′ , h ′ , A ′ (while ( * ) do c done, ρ, h, A ) ρ ′ , h ′ , A ′ Notations: We write h(l, f ) for the value o(f ) such that l ∈ dom(h) and h(l) = o. We write h[(l, f ) → v]
for the heap h ′ that is equal to h except that the f field of the object at location l now has value v. Similarly, ρ[x → v] is the environment ρ modified so that x now maps to v. The object o⋄ is the object satisfying o⋄(f ) = ⋄ for all field f , and ρ⋄ is the environment such that ρ⋄(x) = ⋄ for all variables x. We consider methods with only one parameter and name it p. lookup designates the dynamic lookup procedure that, given a class name cn and a method name m, find the first implementation of m in the class hierarchy starting from the class of name cn and scanning the hierarchy bottom-up. It returns the corresponding method declaration. ret is a specific local variable name that is used to store the result of each method. Reach h (l) (resp. Reach + h (l)) denotes the set of values that are reachable from any sequence (resp. any non-empty sequence) of fields in h. locally allocated locations is updated by both the x := new cn and the x :=m cn:X (y) statements. The execution of an unknown method call x :=?(y) results in a new heap h ′ that keeps all the previous objects that were not reachable from ρ(l). It assigns the variable x a reference that was either reachable from ρ(l) in h or that has been allocated during this call and hence not present in h.

Policies and Inheritance

We impose restrictions on the way that inheritance can interact with copy policies. A method being re-defined in a sub-class can impose further constraints on how fields of the objects returned as result should be copied. A field already annotated deep with policy X must have the same annotation in the policy governing the re-defined method but a field annotated as shallow can be annotated deep for a re-defined method.

Definition 1 (Overriding Copy Policies). A program p is well-formed with respect to overriding copy policies if and only if for any method declaration

Copy(X ′ ) m(x ):= . . . that overrides (i.e. is declared with this signature in a subclass of a class cl ) another method declaration Copy(X) m(x ):= . . . declared in cl , we have

Π p (X) ⊆ Π p (X ′ ).
Example 1. The java.lang.Object class provides a clone() method of policy {} (because its native clone() method is shallow on all fields). A class A declaring two fields f and g can hence override the clone() method and give it a policy {(X, g)}. If a class B extends A and overrides clone(), it must assign it a policy of the form {(X, g); . . . } and could declare the field f as deep. In our implementation, we let the programmer leave the policy part that concerns fields declared in superclasses implicit, as it is systematically inherited.

Semantics of Copy Policies

The informal semantics of the copy policy annotation of a method is:

A copy method satisfies a copy policy X if and only if no memory cell that is reachable from the result of this method following only fields with deep annotations in X, is reachable from another local variable of the caller.

We formalize this by giving, in Fig. 4, a semantics to copy policies based on access paths. An access path consists of a variable x followed by a sequence of field names f i separated by a dot. An access path π can be evaluated to a value v in a context ρ, h with a judgment ρ, h ⊢ π ⇓ v. Each path π has a root variable ↓π ∈ Var . A judgment ⊢ π : τ holds when a path π follows only deep fields in the policy τ .

Access path syntax

π ∈ P ::

= x | π.f Access path evaluation ρ, h ⊢ x ⇓ ρ(x) ρ, h ⊢ π ⇓ l h(l) = o ρ, h ⊢ π.f ⇓ o(f ) Access path root ↓x = x ↓π.f = ↓π

Access path satisfying a policy

We suppose given Πp : Policy id → Policy the set of copy policies of the considered program p.

⊢ x : τ (X1 f1) ∈ τ, (X2 f2) ∈ Πp(X1), • • • , (Xn fn) ∈ Πp(Xn-1) ⊢ x.f1. . . . .fn : τ Policy semantics ∀π, π ′ ∈ P, ∀l, l ′ ∈ Loc, x = ↓π, ↓π ′ = x, ρ, h ⊢ π ⇓ l , ρ, h ⊢ π ′ ⇓ l ′ , ⊢ π : τ    implies l = l ′ ρ, h, x |= τ
(x :=m cn:X (y), ρ 1 , h 1 , A 1 ) ρ 2 , h 2 , A 2 implies ρ 2 , h 2 , x |= τ
Note that because of virtual dispatch, the method executed by such a call may not be the method found in cn but an overridden version of it. The security policy requires that all overriding implementations still satisfy the policy τ .

Lemma 1 (Monotonicity of Copy Policies wrt. Overriding).

τ 1 ⊆ τ 2 implies ∀h, ρ, x, ρ, h, x |= τ 2 ⇒ ρ, h, x |= τ 1
Proof. Under these hypotheses, for all access paths π, ⊢ π : τ 1 implies ⊢ π : τ 2 . Thus the result holds by definition of |=.

Thanks to this lemma, it is sufficient to prove that each method is secure wrt. its own copy signature to ensure that all potential overridings will be also secure.

Type and Effect System

The annotations defined in the previous section are convenient for expressing a copy policy but are not sufficiently expressive for reasoning about the data structures being copied. The static enforcement of a copy policy hence relies on a translation of policies into a graph-based structure (that we shall call types) describing parts of the environment of local variables and the heap manipulated by a program. In particular, the types can express useful alias information between variables and heap cells. In this section, we define the set of types, an approximation (sub-typing) relation ⊑ on types, and an inference system for assigning types to each statement and to the final result of a method.

The set of types is defined using the following symbols:

n ∈ N t ∈ t = N + {⊥, ⊤ out , ⊤} Γ ∈ Var → t ∆ ∈ ∆ = N ⇀ fin Field → t Θ ∈ P(N ) T ∈ T = (Var → t) × ∆ × P(N )
We assume given a set N of nodes. A value can be given a base type t in N + {⊥, ⊤ out , ⊤}. A node n means the value has been locally allocated. The symbol ⊥ means that the value is equal to the null reference ⋄. The symbol ⊤ out means that the value contains a location that cannot reach a locally allocated object. The symbol ⊤ is the specific "no-information" base type. A type is a triplet T = (Γ, ∆, Θ) ∈ T where Γ is a typing environment that maps (local) variables to base types. ∆ is a graph whose nodes are elements of N . The edges of the graphs are labeled with field names. The successors of a node is a base type. Edges over-approximate the concrete points-to relation. Θ is a set of nodes that represents necessarily only one concrete cell each. Nodes in Θ are eligible to strong-update while others (weaks nodes) can only be weakly updated.

In order to link types to the heap structures they represent, we will need to state reachability predicates in the abstract domain. Therefore, the path evaluation relation is extended to types using the following inference rules:

[Γ, ∆] ⊢ x ⇓ Γ (x) [Γ, ∆] ⊢ π ⇓ n [Γ, ∆] ⊢ π.f ⇓ ∆[n, f ] [Γ, ∆] ⊢ π ⇓ ⊤ [Γ, ∆] ⊢ π.f ⇓ ⊤ [Γ, ∆] ⊢ π ⇓ ⊤out [Γ, ∆] ⊢ π.f ⇓ ⊤out
Notice both ⊤ out and ⊤ are considered as sink nodes for path evaluation purposes4 .

From Annotation to Type

The set of all copy policies Π p ⊆ PolicyDecl can be translated into a graph ∆ p as described hereafter. We assume a naming process that associates to each policy name X ∈ Policy id of a program a unique node n ′ X ∈ N .

∆ p = X:{(X1,f1);...;(X k ,f k )}∈Πp (n ′ X , f 1 ) → n ′ X1 , • • • , (n ′ X , f k ) → n ′ X k
Given this graph, a policy τ = {(X 1 , f 1 ); . . . ; (X k , f k )} that is declared in a class cl is translated into a triplet:

Φ(τ ) = n τ , ∆ p ∪ (n τ , f 1 ) → n ′ X1 , • • • , (n τ , f k ) → n ′ X k , {n τ }
Note that we unfold the possibly cyclic graph ∆ p with an extra node n τ in order to be able to catch an alias information between this node and the result of a method, and hence declare n τ as strong. Take for instance the type in Fig. 1: were it not for this unfolding step, the type would have consisted only in a weak node and a ⊤ node, with the variable res mapping directly to the former. Note also that it is not necessary to keep (and even to build) the full graph ∆ p in Φ(τ ) but only the part that is reachable from n τ .

Type Interpretation

The semantic interpretation of types is given in Fig. 5, in the form of a relation

ρ, h, A ∼ [Γ, ∆, Θ]
that states when a local allocation history A, a heap h and an environment ρ are coherent with a type (Γ, ∆, Θ). The interpretation judgment amounts to checking that (i) for every path π that leads to a value l in the concrete memory and to a type t in the graph, the auxiliary type interpretation ρ, h, A , [Γ, ∆] v ∼ t holds; (ii) every strong node in Θ represents a uniquely reachable value in the concrete memory. The auxiliary judgment ρ, h, A , [Γ, ∆] v ∼ t is defined by case on t. The null value is represented by any type. The symbol ⊤ represents any value and ⊤ out those values that do not allow to reach a locally allocated location. A node n represents a locally allocated memory location l such that every concrete path π that leads to l in ρ, h leads to node n in Γ, ∆ . We now establish a semantic link between policy semantics and type interpretation. We show that if the final state of a copy method can be given a type of the form Φ(τ ) then this is a secure method wrt. the policy τ .

Auxiliary type interpretation

ρ, h, A , [Γ, ∆] ⋄ ∼ t ρ, h, A , [Γ, ∆] r ∼ ⊤ Reach h (l) ∩ A = ∅ ρ, h, A , [Γ, ∆] l ∼ ⊤out l ∈ A n ∈ dom(Σ) ∀π, ρ, h ⊢ π ⇓ l ⇒ Γ, Σ ⊢ π ⇓ n ρ, h, A , [Γ, ∆] l ∼ n Main type interpretation ∀π, ∀t, ∀l, [Γ, Σ] ⊢ π ⇓ t ρ, h ⊢ π ⇓ r ⇒ ρ, h, A , [Γ, ∆] r ∼ t ∀n ∈ Θ, ∀π, ∀π ′ , ∀l, ∀l ′ , [Γ, Σ] ⊢ π ⇓ n ∧ [Γ, Σ] ⊢ π ′ ⇓ n ρ, h ⊢ π ⇓ l ∧ ρ, h ⊢ π ′ ⇓ l ′ ⇒ l = l ′ ρ, h, A ∼ [Γ, ∆, Θ]
Fig. 5: Type Interpretation

Theorem 1. Let Φ(τ ) = (n τ , ∆ τ , Θ τ ), ρ ∈ Env , A ∈ P(Loc),
(res) = ρ(x), Γ ′ (res) = n τ and ρ ′ , h, A ∼ [Γ ′ , ∆ τ , Θ τ ], then ρ, h, x |= τ holds.
Proof. We consider two paths π ′ and π such that x = ↓π, ↓π ′ = x, ρ, h ⊢ π ′ ⇓ l, ⊢ π : τ , ρ, h ⊢ π ⇓ l and look for a contradiction. Since ⊢ π : τ , there exists a node

n ∈ ∆ τ such that [Γ ′ , ∆ τ ] ⊢ π ⇓ n. Furthermore ρ ′ , h ⊢ π ⇓ l so we can deduce that l ∈ A.
Thus we obtain a contradiction with ρ, h ⊢ π ′ ⇓ l because any path that starts from a variable other than x cannot reach the elements in A.

Sub-typing

Value sub-typing judgment

t ∈ t ⊥ ≤σ t t ∈ t\N t ≤σ ⊤ ⊤out ≤σ ⊤out n ∈ N n ≤σ σ(n) Main sub-typing judgment σ ∈ N (∆1) → N (∆2) + {⊤} (ST1) ∀t1 ∈ t, ∀π ∈ P, [Γ1, ∆1] ⊢ π ⇓ t1 ⇒ ∃t2 ∈ t, t1 ≤σ t2 ∧ [Γ2, ∆2] ⊢ π ⇓ t2 (ST2) ∀n2 ∈ Θ2, ∃n1 ∈ Θ1, σ -1 (n2) = {n1} (ST3) (Γ1, ∆1, Θ1) ⊑ (Γ2, ∆2, Θ2)

Fig. 6: Sub-typing

To manage control flow merge points we rely on a sub-typing relation ⊑ described in Fig. 6. A sub-type relation (Γ 1 , ∆ 1 , Θ 1 ) ⊑ (Γ 2 , ∆ 2 , Θ 2 ) holds if and only if (ST 1 ) there exists a fusion function σ from dom(∆ 1 ) to dom(∆ 2 ) + {⊤}. σ is a mapping that merges nodes and edges in ∆ 1 such that (ST 2 ) every element t 1 of ∆ 1 accessible from a path π is mapped to an element t 2 of ∆ 2 accessible from the same path, such that t 1 ≤ σ t 2 . In particular, this means that all successors of t 1 are mapped to successors of t 2 . Incidentally, because ⊤ acts as a sink on paths, if t 1 is mapped to ⊤, then all its successors are mapped to ⊤ too. Finally, when a strong node in ∆ 1 maps to a strong node in ∆ 2 , this image node cannot be the image of any other node in ∆ 1 -in other terms, σ is injective on strong nodes (ST 3 ).

Intuitively, it is possible to go up in the type partial order either by merging, or by forgetting nodes in the initial graph. The following example shows three ordered types and their corresponding fusion functions. On the left, we forget the node pointed to by y and hence forget all of its successors (see (ST 2 )). On the right we fusion two strong nodes to obtain a weak node.

f x f x f f x f f y f σ1 σ2
The logical soundness of this sub-typing relation is formally proved with the following theorem.

Theorem 2. For any type T 1 , T 2 ∈ T and state ρ, h, A ,

T 1 ⊑ T 2 and ρ, h, A ∼ [T 1 ] imply ρ, h, A ∼ [T 2 ]
Proof. See [START_REF] Jensen | Secure the clones[END_REF] and the companion Coq development.

Type and Effect System

The type system verifies, statically and class by class, that a program respects the copy policy annotations relative to a declared copy policy. The core of the type system concerns the typability of commands, which is defined through the following judgment:

Γ, ∆, Θ ⊢ c : Γ ′ , ∆ ′ , Θ ′ .
The judgment is valid if the execution of command c in a state satisfying type (Γ, ∆, Θ) will result in a state satisfying (Γ ′ , ∆ ′ , Θ ′ ) or will diverge.

Typing rules are given in Fig. 7. We explain a selection of rules in the following. The rules for if ( * ) then else fi , while ( * ) do done, sequential composition and most of the assignment rules are standard for flow-sensitive type systems. The rule for x := new "allocates" a fresh node n with no edges in the graph ∆ and let Γ (x) reference this node.

There are two rules concerning the instruction x .f :=y for assigning values to fields. If the variable x is represented by node n, then either the node is strong and we update (or add) the edge in the graph ∆ from node n labeled f to point to the value of Γ (y), or it is only weak and we must merge the previous shape with its updated version.

As for method calls, two cases arise depending on whether the method is copyannotated or not. In each case we must also discuss the type of the argument y. On the one hand, if a method is associated with a copy policy τ , we compute the corresponding type (n τ , ∆ τ ) and type the result of x :=m cn:X (y) starting in (Γ, ∆, Θ) with the result type consisting of the environment Γ where x now points to n τ , the heap described by the disjoint union of ∆ and ∆ τ , and the set of strong nodes augmented with n τ . If y is a locally allocated memory location of type n, we must remove all nodes reachable from n, and set all its successors to ⊤. On the other hand, the method is not associated with Command typing rules

Γ, ∆, Θ ⊢ x :=y : Γ [x → Γ (y)], ∆, Θ n fresh in ∆ Γ, ∆, Θ ⊢ x := new cn : Γ [x → n], ∆[(n, ) → ⊥], Θ ∪ {n} Γ (y) = t t ∈ {⊤out , ⊤} [Γ, ∆, Θ] ⊢ x :=y.f : Γ [x → t], ∆, Θ Γ (y) = n Γ, ∆, Θ ⊢ x :=y.f : Γ [x → ∆[n, f ]], ∆, Θ Γ (x ) = n n ∈ Θ Γ, ∆, Θ ⊢ x .f :=y : Γ, ∆[n, f → Γ [y]], Θ Γ (x ) = n n ∈ Θ (Γ, ∆[n, f → Γ [y]], Θ) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) (Γ, ∆, Θ) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) Γ, ∆, Θ ⊢ x .f :=y : Γ ′ , ∆ ′ , Θ ′ Γ, ∆, Θ ⊢ c1 : Γ1, ∆1, Θ1 (Γ1, ∆1, Θ1) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) Γ, ∆, Θ ⊢ c2 : Γ2, ∆2, Θ2 (Γ2, ∆2, Θ2) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) Γ, ∆, Θ ⊢ if ( * ) then c1 else c2 fi : Γ ′ , ∆ ′ , Θ ′ Γ ′ , ∆ ′ , Θ ′ ⊢ c : Γ0, ∆0, Θ0 (Γ, ∆, Θ) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) (Γ0, ∆0, Θ0) ⊑ (Γ ′ , ∆ ′ , Θ ′ ) Γ, ∆, Θ ⊢ while ( * ) do c done : Γ ′ , ∆ ′ , Θ ′ Γ, ∆, Θ ⊢ c1 : Γ1, ∆1, Θ1 Γ1, ∆1, Θ1 ⊢ c2 : Γ2, ∆2, Θ2 Γ, ∆, Θ ⊢ c1; c2 : Γ2, ∆2, Θ2 Πp(X) = τ Φ(τ ) = (nτ , ∆τ ) nodes(∆) ∩ nodes(∆τ ) = ∅ (Γ [y] = ⊥) ∨ (Γ [y] = ⊤out ) Γ, ∆, Θ ⊢ x :=m cn:X (y) : Γ [x → nτ ], ∆ ∪ ∆τ , Θ ∪ {nτ } Πp(X) = τ Φ(τ ) = (nτ , ∆τ ) nodes(∆) ∩ nodes(∆τ ) = ∅ KillSuccn(Γ, ∆, Θ) = (Γ ′ , ∆ ′ , Θ ′ ) Γ [y] = n Γ, ∆, Θ ⊢ x :=m cn:X (y) : Γ ′ [x → nτ ], ∆ ′ ∪ ∆τ , Θ ′ ∪ {nτ } (Γ [y] = ⊥) ∨ (Γ [y] = ⊤out ) Γ, ∆, Θ ⊢ x :=?(y) : Γ [x → ⊤out ], ∆, Θ KillSuccn(Γ, ∆, Θ) = (Γ ′ , ∆ ′ , Θ ′ ) Γ [y] = n Γ, ∆, Θ ⊢ x :=?(y) : Γ ′ [x → ⊤out ], ∆ ′ , Θ ′ Γ, ∆, Θ ⊢ return x : Γ [ret → Γ [x]], ∆, Θ Method typing rule [ • → ⊥][x → ⊤out ], ∅, ∅ ⊢ c : Γ, ∆, Θ Πp(X) = τ Φ(τ ) = (nτ , ∆τ ) (Γ, ∆, Θ) ⊑ (Γ [ret → nτ ], ∆τ , {nτ }) ⊢ Copy(X) m(x ):=c Program typing rule ∀cl ∈ p, ∀md ∈ cl, ⊢ md ⊢ p
Notations: We write ∆[(n, ) → ⊥] for the update of ∆ with a new node n for which all successors are equal to ⊥. We write KillSuccn for the function that removes all nodes reachable from n (with at least one step) and sets all its successors equal to ⊤.

Fig. 7: Type System a copy policy. If the parameter y is null or not locally allocated we know that x points to a non-locally allocated object. Else y is a locally allocated memory location of type n, and we must kill all its successors in the abstract heap. Finally, the rule for method definition verifies the coherence of the result of analysing the body of a method m with its copy annotation Φ(τ ). Type checking extends trivially to all methods of the program.

Note the absence of a rule for typing an instruction x .f :=y when Γ (x ) = ⊤ or ⊤ out . In a first attempt, a sound rule would have been

Γ (x ) = ⊤ Γ, ∆ ⊢ x .f :=y : Γ, ∆[ •, f → ⊤]
Because x may point to any part of the local shape we must conservatively forget all knowledge about the field f . Moreover we should also warn the caller of the current method that a field f of his own local shape may have been updated. We choose to simply reject copy methods with such patterns. Such a strong policy has at least the merit to be easily understandable to the programmer: a copy method should only modify locally allocated objects to be typable in our type system. For similar reasons, we reject methods that attempt to make a method call on a reference of type ⊤ because we can not track side effect modifications of such methods without loosing the modularity of the verification mechanism.

We first establish a standard subject reduction theorem and then prove type soundness. We assume that all methods of the considered program are well-typed.

Theorem 3 (Subject Reduction). Assume T 1 ⊢ c : T 2 and ρ 1 , h 1 , A 1 ∼ [T 1 ]. If (c, ρ 1 , h 1 , A 1 ) ρ 2 , h 2 , A 2 then ρ 2 , h 2 , A 2 ∼ [T 2 ].
Theorem 4. If ⊢ p then all methods m declared in the program p are secure.

For the proofs see [START_REF] Jensen | Secure the clones[END_REF] and the companion Coq development. In this example, we demonstrate the use of the type system on a challenging example taken from the standard Java library. The class java.util.LinkedList provides an implementation of doubly-linked lists. A list is composed of a first cell that points through a field header to a collection of doubly-linked cells. Each cell has a link to the previous and the next cell and also to an element of (parameterized) type E. The clone method provided in java.lang library implements a shallow copy where only cells of type E may be shared between the source and the result of the copy. In Fig. 8 we present a modified version of the original source code: we have inlined all method calls, except those to copy methods and removed exception handling that leads to an abnormal return from methods 5 . Note that one method call in the original code was virtual and hence prevented inlining. Is has been necessary to make a private version of this method. This makes sense because such a virtual call actually constitutes a potentially dangerous hook in a cloning method, as a re-defined implementation could be called when cloning a subclass of Linkedlist.

In Fig. 8 we provide several intermediate types that are necessary for typing this method (T i is the type before executing the instruction at line i). The call to super.clone at line 12 creates a shallow copy of the header cell of the list, which contains a reference to the original list. The original list is thus shared, a fact which is represented by an edge to ⊤ out in type T 13 .

The copy method then progressively constructs a deep copy of the list, by allocating a new node (see type T 14 ) and setting all paths clone.header, clone.header.next and clone.header.previous to point to this node. This is reflected in the analysis by a strong update to the node representing path clone.header to obtain the type T 16 that precisely models the alias between paths clone.header, clone.header.next and clone.header.previous (the Java syntax used here hides the temporary variable that is introduced to be assigned the value of clone.header and then be updated).

This type T 17 is the loop invariant necessary for type checking the whole loop. It is a super-type of T 16 (updated with e → ⊤ out ) and of T 24 which represents the memory at the end of the loop body. The body of the loop allocates a new list cell (pointed to by variable n) (see type T 19 ) and inserts it into the doubly-linked list. The assignment in line 22 updates the weak node pointed to by path n.previous and hence merges the strong node pointed to by n with the weak node pointed to by clone.header, representing the spine of the list. The assignment at line 23 does not modify the type T 23 .

Notice that the types used in this example show that a flow-insensitive version of the analysis could not have found this information. A flow-insensitive analysis would force the merge of the types at all program points, and the call to super.clone return a type that is less precise than the types needed for the analysis of the rest of the method.

Inference

In order to type-check a method with the previous type system, it is necessary to infer intermediate types at each loop header and conditional junction points. A standard approach consists in turning the previous typing problem into a fixpoint problem in a suitable sup-semi-lattice structure. This section presents the lattice that we put on (T , ⊑). Proofs are generally omitted by lack of space but can be found in the companion report. Typability is then checked by computing a suitable least-fixpoint in this lattice. We end this section by proposing a widening operator that is necessary to prevent infinite iterations.

We write ≡ for the equivalence relation defined by T 1 ≡ T 2 if and only if T 1 ⊑ T 2 and T 2 ⊑ T 1 . Although this entails that ⊑ is a partial order structure on top of (T , ≡), equality and order testing remains difficult using only this definition. Instead of considering the quotient of T with ≡, we define a notion of well-formed types on which ⊑ is antisymmetric. To do this, we assume that the set of nodes, variable names and field names are countable sets and we note n i (resp. x i and f i ) the ith node (resp. variable and field). A type (Γ, ∆, Θ) is well-formed if every node in ∆ is reachable from a node in Γ and the nodes in ∆ follow a canonical numbering based on a breadth-first traversal of the graph. Any type can be garbage-collected into a canonical well-formed type by removing all unreachable nodes from variables and renaming all remaining nodes using a fixed strategy based on a total ordering on variable names and field names and a breadth-first traversal. We note GC this transformation. The following example shows the effect of GC using a canonical numbering.

x 1 ⊥ ⊥ x 2 x 3 f 1 f 2 f 2 f 1 f 1 f 2 f 1 f 2 f 1 x 1 ⊥ ⊥ x 2 x 3 f 1 f 2 f 2 f 1 f 1 f 2 f 1 f 2 n1 n2 n3 n4 n5 gc f 2
Since by definition, ⊑ only deals with reachable nodes, the GC function is a ≡morphism and respects type interpretation. This means than inference engine can at any time replace a type by a garbage-collected version. This is useful to perform an equivalence test in order to check fixpoint iteration ending.

Lemma 2. For all well-formed types

T 1 , T 2 ∈ T , T 1 ≡ T 2 iff T 1 = T 2 .
Definition 3. Let ⊔ be an operator that merges two types according to the algorithm in Fig. 9.

/ / I n i t i a l i z a t i o n . / / α-n o d e s a r e s e t s i n t . / / αt r a n s i t i o n s c a n be / / non-d e t e r m i n i s t i c . α = lift(Γ1,Γ2,∆1 ∪ ∆2) / / S t a r t w i t h e n v i r o n m e n t s . for {(x, t); (x, t ′ )} ⊆ (Γ1 × Γ2) { fusion({t, t ′ }) } / / P r o p a g a t e i n α . α, where nodes are labelled by sets of elements in t. This operation is performed by the lift function, that maps nodes to singleton nodes, and fields to transitions.

while ∃f ∈ Field, ∃u ∈ α, |succ(u, f )| > 1 { fusion(succ(u,f )) } / / R
) → u] } if ∃n ′ , α(n ′ , f ) = t { / / Re-r o u t e i n b o u n d e d g e s . α ← α[(n ′ , f ) → N ] }} α ← α -u }}
2. It joins together the nodes in α referenced by Γ i using the fusion algorithm 6 .

3. Then it scans the NDG and merges all nondeterministic successors of nodes. 4. Finally it uses the ground function to recreate a graph ∆ from the now-deterministic graph α. This function operates by pushing a node set to a node labelled by the ≤ σ -sup of the set. The result environment Γ is derived from Γ i and α before the ∆-reconstruction.

All state fusions are recorded in a map σ which binds nodes in ∆ 1 ∪ ∆ 2 to nodes in ∆.

Theorem 5. The operator ⊔ defines a sup-semi-lattice on types.

Proof. See [START_REF] Jensen | Secure the clones[END_REF].

The poset structure does not enjoy the ascending chain condition. The following chain is an example infinite ascending chain.

f ⊥ x ... x ⊥ f x ⊥ f ... ...
We have then to rely on a widening [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] operator to enforce termination of fixpoint computation. Here we follow a very pragmatic approach and define a widening operator ∇ ∈ T × T → T that takes the result of ⊔ and that collapses together (with the operator fusion defined above) any node n and its predecessors such that the minimal path reaching n and starting from a local variable is of length at least 2.

Experiments

The policy language and its enforcement mechanism has been implemented in the form of a security tool for Java byte code. Standard Java @interface declarations are used to specify native annotations, which enable development environments such as Eclipse or Netbeans to parse, identify and auto-complete @Shallow, @Deep, and @Copy tags. Source code annotations are being made accessible to bytecode analysis frameworks.

Both the policy extraction and enforcement components are implemented using the Javalib/Sawja static analysis libraries 7 to derive annotations and intermediate code representations.

In its standard mode, the tool performs a modular verification of annotated classes. We have run experiments on several classes of the standard library (specially in the package java.util) and have successfully checked realistic copy signatures for them (see the companion web page for examples). These experiments have also confirmed that the policy enforcement mechanism facilitates re-engineering into more compact implementations of cloning methods in classes with complex dependencies, such as those forming the gnu.xml.transform package. For example, in the Stylesheet class an inlined implementation of multiple deep copy methods for half a dozen fields can be rewritten to dispatch these functionalities to the relevant classes, while retaining the expected copy policy. This is made possible by the modularity of our enforcement mechanism, which validates calls to external cloning methods as long as their respective policies have been verified. However, some cloning methods will necessarily be beyond the reach of the analysis. We have identified one such method in GNU Classpath's TreeMap class, where the merging of information at control flow merge points destroys too much of the inferred type graph. A disjunctive form of abstraction seems necessary to verify a deep copy annotation on such programs and we leave this as a challenging extension.

The analysis is also capable of processing un-annotated methods, albeit with less precision than when copy policies are available-this is because it cannot rely on annotations to infer external copy method types. Nevertheless, this capability allows us to test our tool on two large code bases. The 17000 classes in Sun's rt.jar and the 7000 in the GNU Classpath have passed our scanner un-annotated. Among the 459 clone() methods we found in these classes, only 15 have been rejected because of an illegal assignment or method call and we were unable to infer the minimal signatures {} (the same signature as java.lang.Object.clone()) in 78 methods. Our prototype confirms the efficiency of the enforcement technique because all these verifications took only 25s on a laptop computer.

Our prototype, the Coq formalization and proofs, as well as examples of annotated classes can be found at http://www.irisa.fr/celtique/ext/clones.

Related Work

Several proposals for programmer-oriented annotations of Java programs have been published following Bloch's initial proposal of an annotation framework for the Java language [START_REF] Bloch | JSR 175: A metadata facility for the Java programming language[END_REF]. These proposals define the syntax of the annotations but often leave their exact semantics unspecified. A notable exception is the set of annotations concerning non-null annotations [START_REF] Fähndrich | Declaring and checking non-null types in an objectoriented language[END_REF] for which a precise semantic characterization has emerged [START_REF] Hubert | Semantic foundations and inference of non-null annotations[END_REF]. Concerning security, the GlassFish environment in Java offers program annotations of members of a class (such as @DenyAll or @RolesAllowed) for implementing rolebased access control to methods.

To the best of our knowledge, the current paper is the first to propose a formal, semantically founded framework for secure cloning through program annotation and static enforcement. The closest work in this area is that of Anderson et al. [START_REF] Anderson | Lightweight annotations for controlling sharing in concurrent data structures[END_REF] who have designed an annotation system for C data structures in order to control sharing between threads. Annotation policies are enforced by a mix of static and run-time verification. On the run-time verification side, their approach requires an operator that can dynamically "cast" a cell to an unshared structure. In contrast, our approach offers a completely static mechanism with statically guaranteed alias properties.

Aiken et al. proposes an analysis for checking and inferring local non-aliasing of data [START_REF] Aiken | Checking and inferring local non-aliasing[END_REF]. They propose to annotate C function parameters with the keyword restrict to ensure that no other aliases to the data referenced by the parameter are used during the execution of the method. A type and effect system is defined for enforcing this discipline statically. This analysis differs from ours in that it allows aliases to exist as long as they are not used whereas we aim at providing guarantees that certain parts of memory are without aliases. The properties tracked by our type system are close to escape analysis [START_REF] Blanchet | Escape analysis for object-oriented languages: Application to Java[END_REF][START_REF] Choi | Escape analysis for java[END_REF] but the analyses differ in their purpose. While escape analysis tracks locally allocated objects and tries to detect those that do not escape after the end of a method execution, we are specifically interested in tracking locally allocated objects that escape from the result of a method, as well as analyse their dependencies with respect to parameters.

Our static enforcement technique falls within the large area of static verification of heap properties. A substantial amount of research has been conducted here, the most prominent being region calculus [START_REF] Tofte | Region-based memory management[END_REF], separation logic [START_REF] O'hearn | Separation and information hiding[END_REF] and shape analysis [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF]. Of these three approaches, shape analysis comes closest in its use of shape graphs. Shape analysis is a large framework that allows to infer complex properties on heap allocated data-structures like absence of dangling pointers in C or non-cyclicity invariants. In this approach, heap cells are abstracted by shape graphs with flexible object abstractions. Graph nodes can either represent a single cell, hence allowing strong updates, or several cells (summary nodes). Materialization allows to split a summary node during cell access in order to obtain a node pointing to a single cell. The shape graphs that we use are not intended to do full shape analysis but are rather specialized for tracking sharing in locally allocated objects. We use a different naming strategy for graph nodes and discard all information concerning non-locally allocated references. This leads to an analysis which is more scalable than full shape analysis, yet still powerful enough for verifying complex copy policies as demonstrated in the concrete case study java.util.LinkedList.

Conclusions and Perspectives

Cloning of objects is an important aspect of exchanging data with untrusted code. Current language technology for cloning does not provide adequate means for defining and enforcing a secure copy policy statically; a task which is made more difficult by important object-oriented features such as inheritance and re-definition of cloning methods. We have presented a flow-sensitive type system for statically enforcing copy policies defined by the software developer through simple program annotations. The annotation formalism is compatible with the inheritance-based object oriented programing language and deals with dynamic method dispatch. The verification technique is designed to enable modular verification of individual classes, in order to provide a framework that can form part of an extended, security-enhancing Java byte code verifier. By specifically targeting the verification of copy methods, we consider a problem for which it is possible to deploy a localized version of shape analysis that avoids the complexity of a full shape analysis framework.

The present paper constitutes the formal foundations for a secure cloning framework. All theorems except those of Section 4 have been mechanized in the Coq proof assistant. Mechanization has been of great help to get right the soundness arguments but has been made particularly challenging because of the storeless nature of our type interpretation.

Several issues merit further investigations in order to develop a full-fledged software security verification tool. In the current approach, virtual methods without copy policy annotations are considered as black boxes that may modify any object reachable from its arguments. An extension of our copy annotations to virtual calls should be worked out if we want to enhance our enforcement technique and accept more secure copying methods. More advanced verifications will be possible if we develop a richer form of type signatures for methods where the formal parameters may occur in copy policies, in order to express a relation between copy properties of returning objects and parameter fields. The challenge here is to provide sufficiently expressive signatures which at the same time remain humanly readable software contracts. The current formalisation has been developed for a sequential model of Java. We believe that the extension to interleaving multi-threading semantics would be feasible without major changes to the type system because we only manipulate thread-local pointers. Spelling out the formal details of this argument is left for further work.

Fig. 1 :

 1 Fig. 1: A linked structure (left part) and its abstraction (right part).

x

  , y ∈ Var f ∈ Field m ∈ Meth cn ∈ Classid X ∈ Policy id p ∈ Prog ::= cl cl ∈ Class ::= class cn [extends cn] {pd md } pd ∈ PolicyDecl ::= X : {τ } τ ∈ Policy ::= (X, f ) md ∈ MethDecl ::= Copy(X) m(x ):=c c ∈ Comm ::= x :=y | x :=y.f | x .f :=y | x :=null | x := new cn | x :=m cn:X (y) | x :=?(y) | return x | c; c | if ( * ) then c else c fi | while ( * ) do c done Notations: We write for the reflexive transitive closure of the subclass relation induced by a (well-formed) program that is fixed in the rest of the paper. We write x a sequence of syntactic elements of form x.

Fig. 2 :

 2 Fig. 2: Language Syntax.

Fig. 3 :

 3 Fig. 3: Semantic Rules.

Fig. 4 :

 4 Fig. 4: Copy Policy Semantics

Fig. 8 :

 8 Fig. 8: Intermediate Types for java.util.LinkedList.clone()

Fig. 9 :

 9 Fig. 9: Join AlgorithmThe procedure has T 1 = (Γ 1 , ∆ 1 , Θ 1 ) and T 2 = (Γ 2 , ∆ 2 , Θ 2 ) as input, then takes the following steps.1. It first makes the disjunct union of ∆ 1 and ∆ 2 into a non-deterministic graph (NDG) α, where nodes are labelled by sets of elements in t. This operation is performed by the lift function, that maps nodes to singleton nodes, and fields to transitions.

To be type-checked by the Java compiler it is necessary to add a cast before calling clone() on value. A cast to a sub interface of Cloneable that declares a clone() method is necessary.

Our implementation uses a sightly different policy declaration syntax because of the limitations imposed by the Java annotation language.

We note ⇀fin for partial functions on finite domains.

The sink nodes status of ⊤ (resp. ⊤out ) can be understood as a way to state the following invariant enforced by our type system: when a cell points to an unspecified (resp. foreign) part of the heap, all successors of this cell are also unspecified (resp. foreign).

Inlining is automatically performed by our tool and exception control flow graph is managed as standard control flow but omitted here for simplicity.

Remark that Γi-bindings are not represented in α, but that node set fusions are trivially traceable. This allows us to safely ignore Γi during the following step and still perform a correct graph reconstruction.

[START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] http://sawja.inria.fr

* This work was supported by the ANSSI, the ANR, and the Région Bretagne, respectively under the Javasec, Parsec, and Certlogs projects.


D Pressnitzer

J M Hupé

Temporal dynamics of auditory and visual bistability reveal common principles of perceptual organization

When dealing with natural scenes, sensory systems have to process an often messy and ambiguous flow of information. A stable perceptual organization has nevertheless to be achieved in order to guide behavior. The neural mechanisms involved can be highlighted by intrinsically ambiguous situations. In such cases, bistable perception occurs: distinct interpretations of the unchanging stimulus alternate spontaneously in the mind of the observer [1]. Bistable stimuli have been used extensively for more than two centuries to study visual perception [2]. Here we demonstrate that bistable perception also occurs in the auditory modality. We compared the temporal dynamics of percept alternations observed during auditory streaming [3, 4] with those observed for visual plaids [5, 6], and the susceptibilities of both modalities to volitional control. Strong similarities indicate that auditory and visual alternations share common principles of perceptual bistability. The absence of correlation across modalities for subjectspecific biases, however, suggests that these common principles are implemented at least partly independently across sensory modalities. We propose that visual and auditory perceptual organization could rely on distributed but functionally similar neural competition mechanisms aimed at resolving sensory ambiguities.

Results and Discussion

The study of bistable perception has generated a sustained interest in visual neuroscience, as it decouples the conscious perception of the observer from the characteristics of the physical stimulation: the same stimulus evokes different percepts. This provides a powerful method to probe the neural bases of perception.

Changes in neural responses that correlate with subjective percepts cannot be traced to changes in the stimulation [START_REF] Parker | Sense and the single neuron: probing the physiology of perception[END_REF]. Bistability has been described with a wide range of stimuli: ambiguous figures [START_REF] Long | Enduring interest in perceptual ambiguity: alternating views of reversible figures[END_REF], binocular rivalry [START_REF] Alais | Binocular Rivalry[END_REF][START_REF] Blake | Visual competition[END_REF], moving plaids [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF] to cite a few. Some theoretical accounts of bistability are based on sensory fatigue, adaptation or inhibition of peripheral neural channels, and are thus specific to the type of bistability studied [START_REF] Blake | A neural theory of binocular rivalry[END_REF][START_REF] Blake | Visual motion retards alternations between conflicting perceptual interpretations[END_REF][START_REF] Lehky | An astable multivibrator model of binocular rivalry[END_REF]. Others posit a central switching mechanism [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF][START_REF] Carter | A common oscillator for perceptual rivalries?[END_REF]. Neural correlates have been exhibited for both types of models [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF][START_REF] Long | Enduring interest in perceptual ambiguity: alternating views of reversible figures[END_REF][START_REF] Blake | Visual competition[END_REF][START_REF] Tong | Competing theories of binocular rivalry: A possible resolution[END_REF].

In spite of the value that bistable perception presents for the study of perceptual organization, it has only been described systematically in the visual modality. There are reports of alternating perceptual interpretations of an unchanging auditory stimulation, such as in the verbal transformation effect where the repetition of a same word can produce different meanings [START_REF] Warren | An auditory analogue of the visual reversible figure[END_REF], or for auditory grouping [START_REF] Van Noorden | Temporal Coherence in the Perception of Tone Sequences[END_REF]. It is unclear, however, what similarities or differences exist between such phenomena and visual bistability. The present study of bistable perception in two sensory modalities aims to investigate whether the rules governing the alternation of perceptual states are general principles of brain function, or specific to the visual system.

We chose a simple auditory scene to study "auditory bistability". We used a stimulus where a high-frequency tone A alternates with a low-frequency tone B, in repeated ABA-patterns. Listeners report either hearing the sequence as one stream ABA-ABA or as two streams A-A-A-A and -B---B-. This streaming stimulus has become a canonic paradigm to study auditory scene analysis behaviorally [START_REF] Bregman | Auditory Scene Analysis: The Perceptual Organization of sound[END_REF][START_REF] Van Noorden | Temporal Coherence in the Perception of Tone Sequences[END_REF], or, recently, to address the neural basis of auditory scene analysis [START_REF] Fishman | Neural correlates of auditory stream segregation in primary auditory cortex of the awake monkey[END_REF][START_REF] Micheyl | Perceptual organization of tone sequences in the auditory cortex of awake macaques[END_REF][START_REF] Gutschalk | Neuromagnetic correlates of streaming in human auditory cortex[END_REF][START_REF] Cusack | The intraparietal sulcus and perceptual organization[END_REF][START_REF] Bee | Primitive auditory stream segregation: a neurophysiological study in the songbird forebrain[END_REF]. Three of these studies took advantage of spontaneous percept alternations to look for corresponding changes in neural activity [START_REF] Micheyl | Perceptual organization of tone sequences in the auditory cortex of awake macaques[END_REF][START_REF] Gutschalk | Neuromagnetic correlates of streaming in human auditory cortex[END_REF][START_REF] Cusack | The intraparietal sulcus and perceptual organization[END_REF]. It seems timely to assess the commonalities of this phenomenon with visual bistability, which has been the subject of intense investigation.

Moving plaids were chosen as visual stimuli. When a network of crossing lines is seen moving through a circular aperture, it can be perceived either as a single plaid moving in a given direction or as two gratings sliding in opposite directions on top of each other [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF][START_REF] Wallach | Uber visuelle wahrgenommene Bewegungsrichtung[END_REF]. Plaids are typical illustrations of visual bistability, with similar characteristics to binocular rivalry [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF][START_REF] Rubin | Dynamics of perceptual bi-stability: plaids and binocular rivalry compared[END_REF][START_REF] Sheppard | Plaid Motion Rivalry: correlates with binocular rivalry and positive mood state[END_REF] but displaying less indeterminate percepts (blending or piecemeal rivalry). Moreover, there is a formal correspondence between the visual and auditory stimuli chosen in terms of organization of the sensory scene: a decision has to be made whether to group the scene into one stream/one plaid, or to split the scene between two streams/two gratings. We will refer to these situations as Grouped or Split percepts. Examples of auditory and visual stimuli are provided as Supplemental Data.

Leopold and Logothetis [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF] established three characteristics of perceptual alternations observed in all instances of visual bistability: exclusivity, randomness, and inevitability. Exclusivity means that perceptual interpretations are mutually exclusive. Randomness characterizes the statistical distribution of the time spent in each percept. Inevitability indicates that observers have only limited volitional control on perceptual alternations. We now show that these criteria are met for both auditory and visual ambiguous stimuli, with similar characteristics in their temporal dynamics.

Exclusivity

Twenty-three participants listened to ABA-sequences or observed moving plaids for 4-minute intervals. They were instructed to report continuously their conscious perception (Grouped, Split, or Indeterminate). All participants reported spontaneous alternations during prolonged exposure to either type of stimuli. In the auditory case, the time spent in the Grouped or Split percepts was equally divided on average across the population of participants. This proportion is expected to depend on the parameters chosen for the ABA-stimulus [START_REF] Bregman | Auditory Scene Analysis: The Perceptual Organization of sound[END_REF]. Importantly, very little time was spent in an "indeterminate" perceptual state: less than 3 % of total presentation time, even though this was the default response when stimulus presentation began. Mean and standard deviation for the percentage of time spent were: Grouped 51.4 (21.2); Split 45.8 (20.4); Indeterminate 2.8 (3.5). Results were similar in the visual modality: Grouped 50.1 (14.6); Split 48.5 (15.1); Indeterminate 1.3 (2.0). Both modalities thus display the basic feature of bistability, the spontaneous alternation between mutually exclusive percepts.

Randomness

A hallmark of visual bistability is that the durations of alternating percepts, or phases, follow a random law that can be fitted with a gamma or lognormal distribution [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF][START_REF] Lehky | Binocular rivalry is not chaotic[END_REF][START_REF] Zhou | Perceptual dominance time distributions in multistable visual perception[END_REF]. A lognormal distribution suggests the multiplication of a large number of independent random processes [START_REF] Zhou | Perceptual dominance time distributions in multistable visual perception[END_REF] whereas a gamma distribution results from the combination of a small number of consecutive Poisson processes [START_REF] Murata | Discrete stochastic process underlying perceptual rivalry[END_REF]. Although observed for a variety of phenomena, lognormal or gamma distributions are not observed when subjects are asked to press buttons randomly [START_REF] Leopold | Brain mechanisms of visual awareness[END_REF]. (A,B) The durations of the first seven successive phases are presented for both the auditory modality (A, dark grey) and the visual modality (B, light grey). Durations were first transformed to a log scale, then averaged across all participants that experienced 7 or more successive phases (Audition N=20, Vision N=23). The error bars represent 95% confidence intervals around the mean estimated by 1.96 standard error. The logscale is converted back to seconds for display purposes. The first percept is significantly longer that subsequent ones. There is no long-term trend in the duration of phases after the first one. (C, D) The histograms of durations of Grouped and Split phases are presented, compiled for all participants (N=23) and percept types (Grouped and Split). All durations were normalized by the average phase duration in each given run. The first phase was excluded from the analysis as it lasted longer than subsequent ones. There is no significant difference between the distributions for the two modalities (Kolmogorov-Smirnov test, p=0.1). (E, F) The duration of a percept is shown as a function of the duration of the previous percept, for all participants (N=23). These are the same data that constitute the histograms of panels C, D, but in raw format without any normalization. The duration of a phase does not influence the duration of the next phase, for both modalities. All data in this figure from the Neutral task.

The average durations for successive phases are shown in Figure 1A,B. For both the auditory and visual modalities, the first phase had a longer duration than subsequent phases. This is consistent with previous results obtained in the visual modality [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF]. With the first phase excluded, the switching rate was constant over observation time with no long-term trends (see also Supplemental Data). There is a tendency for auditory phases to last longer than visual ones, which might be due to the specific stimulus parameters used here.

The distribution of phase durations for the auditory and visual modality are illustrated in Figure 1C, D. Analyses of phase distribution require that switching rate be stable over time so the first percept was excluded. Phases were normalized by the average phase duration over a given trial to limit the influence of inter-individual differences, as proposed for visual bistability [START_REF] Rubin | Dynamics of perceptual bi-stability: plaids and binocular rivalry compared[END_REF][START_REF] Logothetis | What is rivalling during binocular rivalry?[END_REF]. The normalized phase distributions are skewed toward longer durations, a characteristic of gamma or lognormal distributions. Distinguishing between the two is beyond the scope of the present paper where only potential similarities between auditory and visual distributions are of interest. An analysis of variance (Experimental Procedures) showed that both distributions were not statistically different from lognormal. A Kolmogorov-Smirnov test further indicated that the auditory distribution was not significantly different from the visual distribution. The temporal dynamics of both phenomena thus display a strong similarity.

Scatterplots of the duration of a given phase as a function of the duration of the previous phase are shown in Figure 1E, F. These panels displays all available data points and illustrate the large variability observed among phase durations when no normalization is applied. No correlation exists between successive durations, consistent with what is observed for binocular rivalry [START_REF] Lehky | Binocular rivalry is not chaotic[END_REF] (statistical analyses as Supplemental Data).

Inevitability

Volitional control can bias the perception of some visual bistable stimuli [START_REF] Von Helmholtz | Treatise on Physiological Optics[END_REF][START_REF] Lack | Selective Attention and the Control of Binocular Rivalry[END_REF][START_REF] Meng | Can attention selectively bias bistable perception? Differences between binocular rivalry and ambiguous figures[END_REF][START_REF] Van Ee | Voluntary control and the dynamics of perceptual bi-stability[END_REF].

The amount of volitional control that can be exerted has been proposed as an indication of the neural level where competition between percepts occurs, with large control reflecting higher-level processes [START_REF] Long | Enduring interest in perceptual ambiguity: alternating views of reversible figures[END_REF]. We investigated the effect of observer intention on the reported percepts for auditory streaming and visual plaids. On successive runs, participants were instructed to try to maintain a given perceptual interpretation throughout stimulus presentation. For both modalities, volitional control had a significant effect (Figure 2A). When subjects tried to group, the proportion of Grouped percepts increased as compared to the neutral task. The opposite was true when they tried to split. The effect of volitional control was stronger for the auditory modality than for the visual modality. Bistable perception is however inevitable in the two modalities, as alternations persist even in the presence of intention.

Figure 2 Effect of volitional control on auditory and visual bistability. (A)

The proportion of time spent in the Grouped percept is shown as a function of the task (Neutral, Group, Split) and modality of presentation (Auditory in dark grey, Visual in light grey). Mean and 95% confidence intervals across participants. Data for all participants (N=23). Each participant performed each task once. In the Neutral task, the Grouped percept was experienced for about 50% of the time on average, for both modalities. Participants could influence the amount of time spent in a given perceptual state according to their intention. The effect is observed in both modalities with a stronger magnitude in the auditory modality (Group minus Split difference 53% vs 20%). (B, C) The time spent in Grouped (solid lines) and Split (dashed lines) percept is shown as a function of the task, for each modality. Durations were converted to a log-scale, with the corresponding values shown in seconds for display purposes. Mean and 95 % confidence intervals across participants. In both modalities and for both volitional tasks, intention translated into a shortening of the duration of the unwanted percept but caused no increase in the duration of the target percept Volitional control had a specific effect on the duration of each percept type (Figure 2B,C). In the neutral task, no difference was found between the Grouped and Split durations. When subjects tried to group, the mean duration of the Grouped phases did not actually increase -rather, the mean duration of the Split phases was reduced. This pattern of result is identical for the two intentions and the two modalities: volitional control shortens the unwanted phases but does not increase the duration of the target phases. This systematic and somewhat counter-intuitive effect argues against unspecific demand characteristic biases, where observers would simply adjust their reports to what the experimenter is asking for. It is rather consistent with Levelt's second proposition [START_REF] Levelt | On Binocular Rivalry[END_REF]. This proposition states that, for binocular rivalry, strengthening the stimulus to one eye does not affect the dominance duration of that eye but rather decreases the dominance duration of the other eye. If it is assumed that intention increases the perceptual strength of the target percept, then the current data conform to Levelt's second proposition. A similar effect of intention, although smaller, can be observed for binocular rivalry as selective attention only decreases the unattended eye dominance duration [START_REF] Meng | Can attention selectively bias bistable perception? Differences between binocular rivalry and ambiguous figures[END_REF].

Absence of correlation across modalities

An important debate about visual bistability concerns the possibility of a common, top-down neural mechanism as the cause of alternations for all ambiguous stimuli [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF][START_REF] Long | Enduring interest in perceptual ambiguity: alternating views of reversible figures[END_REF][START_REF] Blake | Visual competition[END_REF][START_REF] Von Helmholtz | Treatise on Physiological Optics[END_REF]. A common mechanism should introduce subject-specific biases irrespective of the stimulus [START_REF] Carter | A common oscillator for perceptual rivalries?[END_REF][START_REF] Sheppard | Plaid Motion Rivalry: correlates with binocular rivalry and positive mood state[END_REF]. The number of switches [START_REF] Carter | A common oscillator for perceptual rivalries?[END_REF], proportion of Grouped percept, and effect of volitional control [START_REF] Meng | Can attention selectively bias bistable perception? Differences between binocular rivalry and ambiguous figures[END_REF] were compared for each subject across the two modalities in the present data. Inter-subject variations were large on all of these measures (Figure 3) so they can potentially reveal subject-specific biases. There was a weak, non-significant correlation for the number of switches (Figure 3A) indicating no bias to switch quickly or slowly irrespective of sensory modality-unlike the strong correlation observed between different visual bistable stimuli [START_REF] Carter | A common oscillator for perceptual rivalries?[END_REF][START_REF] Sheppard | Plaid Motion Rivalry: correlates with binocular rivalry and positive mood state[END_REF]. The proportion of Grouped percept was also uncorrelated across modalities (Figure 3B). Finally, the amount of effective volitional control was estimated by subtracting the proportion of Grouped percepts between the "group" and "split" intentions, for each observer (Figure 3C). This measure was unrelated across modalities. Observers who were better at controlling their auditory percepts were not necessarily better at controlling their visual percepts (bottom-right part of Figure 3C). For all three measures investigated, idiosyncratic biases did not carry over between visual and auditory bistability.

Auditory streaming as a bistable percept

Auditory streaming determines whether we assign a sequence of sounds to one or more sources. Whereas streaming usually reflects physical reality, such as when more than one person talk at the same time, it can also be fooled, for instance when two interleaved musical melodies are produced by a monophonic instrument. With the ABA-stimulus that we used, there is an irresolvable ambiguity as to how many streams should be perceived. This leads to spontaneous alternations between percepts of one or two streams when the stimulus is heard for a prolonged period of time [START_REF] Van Noorden | Temporal Coherence in the Perception of Tone Sequences[END_REF].

In addition, we have shown that these alternations share many features with visual bistability [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF]: percepts of one-stream vs two-streams are mutually exclusive, their duration follows a lognormal distribution with short-term independence and no longterm trend, and volitional control has an influence on but does not abolish alternations. Based on these strong similarities, we propose that auditory streaming can be considered as an instance of perceptual bistability.

The bistable nature of auditory streaming has not been recognized before. Anstis and Saida [START_REF] Anstis | Adaptation to Auditory Streaming of Frequency-Modulated Tones[END_REF] reported a "marked long-term trend over time toward auditory segregation", and concluded that streaming was not comparable to visual bistability for which no such trend is observed. They used 30-sec long stimuli, however, and most experimenters used even shorter presentation times. The longer observation periods chosen here (240 sec), together with the analysis methods normally applied to visual bistability, lead on the contrary to the conclusion that after the first percept, the steady-state of the temporal dynamics of auditory streaming is purely stochastic with no long-term trend (Figure 1A). This provides an alternative framework to interpret the long-term build-up of streaming documented by numerous studies [START_REF] Cusack | Effects of location, frequency region, and time course of selective attention on auditory scene analysis[END_REF]. A bias for an initial Grouped percept that lasts longer than subsequent ones was observed here (in the two modalities, possibly due to the asymmetry between Grouped and Split percepts).

When such an initial Grouped bias is combined with random phase duration, averages across listeners and/or repeats will exhibit a gradual increase in the proportion of Split reports. The subsequent purely bistable nature of phase alternations then produces a plateau corresponding to the steady-state probabilities of the percepts. These two features are fully consistent with characteristics of the build-up of streaming, when considering average measures [START_REF] Bregman | Auditory Scene Analysis: The Perceptual Organization of sound[END_REF][START_REF] Cusack | Effects of location, frequency region, and time course of selective attention on auditory scene analysis[END_REF]. Our results suggest that, additionally, measures of temporal dynamics [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF] could provide valuable new tools in the investigation of auditory streaming.

Models of perceptual bistability

Current accounts of visual bistability emphasize low-level competition of features [START_REF] Blake | A neural theory of binocular rivalry[END_REF][START_REF] Lehky | An astable multivibrator model of binocular rivalry[END_REF], high-level competition of representations [START_REF] Logothetis | What is rivalling during binocular rivalry?[END_REF], or top-down attentional selection mechanisms [START_REF] Leopold | Multistable phenomena: changing views in perception[END_REF][START_REF] Von Helmholtz | Treatise on Physiological Optics[END_REF]. The question arises as to which of those theoretical frameworks is able to account for both visual and auditory bistability.

We observed strong similarities between bistability in the two sensory modalities.

A first possibility is that both phenomena are controlled by a common, high-level switching mechanism, as has been hypothesized for various kinds of visual bistability [START_REF] Carter | A common oscillator for perceptual rivalries?[END_REF]. Using fMRI with auditory streaming stimuli, Cusack [START_REF] Cusack | The intraparietal sulcus and perceptual organization[END_REF] registered activation in the intraparietal sulcus correlated with the subjective experience of Split percepts. As the intraparietal sulcus is likely involved in cross-modal integration [START_REF] Calvert | Crossmodal processing in the human brain: insights from functional neuroimaging studies[END_REF], it could contribute to bistability in both modalities.

We failed to observe, however, consistent observer-specific biases across modalities. Strong biases would be expected if a single top-down selection mechanism were the sole determinant of the auditory and visual bistability. Another possibility is that some mechanisms of competition between percepts are distributed across modalities, but share common functional principles. In the visual domain, a canonic brain architecture of mutual inhibition between populations of neurons coding for various attributes could explain the similarities between different types of bistability [START_REF] Rubin | Dynamics of perceptual bi-stability: plaids and binocular rivalry compared[END_REF]. Inhibition has also been proposed as a functional building block for auditory scene analysis [START_REF] Pressnitzer | Physiological correlates of comodulation masking release in the mammalian ventral cochlear nucleus[END_REF]. Distributed competition, as a general computational process, would be useful to resolve perceptual ambiguities irrespective of sensory modality.

Neurophysiological evidence for distributed competition

The hypothesis of distributed competition is consistent with findings of neural correlates of the perception of ambiguous visual stimuli at different levels of neural processing. Using fMRI, correlates of competition have been observed in V1 for binocular rivalry [START_REF] Tong | Interocular rivalry revealed in the human cortical blind-spot representation[END_REF][START_REF] Polonsky | Neuronal activity in human primary visual cortex correlates with perception during binocular rivalry[END_REF][START_REF] Lee | Traveling waves of activity in primary visual cortex during binocular rivalry[END_REF] as well as other types of visual bistability [START_REF] Muckli | Primary visual cortex activity along the apparent-motion trace reflects illusory perception[END_REF][START_REF] Murray | Shape perception reduces activity in human primary visual cortex[END_REF].

Competition between interpretations is also reflected, however, in neuronal populations that code for the specific attributes that are competing: the human fusiform face area and the parahippocampal place area for binocular rivalry between faces and houses [START_REF] Tong | Binocular rivalry and visual awareness in human extrastriate cortex[END_REF], or areas involved in motion processing for rivalry between motion stimuli [START_REF] Moutoussis | A binocular rivalry study of motion perception in the human brain[END_REF]. Single units recordings in awake macaques also demonstrated correlations with perceptual alternations at different level of the visual cortex [START_REF] Leopold | Activity changes in early visual cortex reflect monkeys' percepts during binocular rivalry[END_REF], specifically in area MT for moving stimuli [START_REF] Logothetis | Neuronal correlates of subjective visual perception[END_REF] or in the temporal cortex for more complex objects [START_REF] Sheinberg | The role of temporal cortical areas in perceptual organization[END_REF].

Similarly, neural correlates of auditory streaming have been observed at different processing stages. Recordings in primary auditory areas with the ABA-stimulus showed that units with receptive fields centered on the A-tones displayed a reduced response to the B-tones when Split percepts were more likely. This was observed in the primary auditory cortex of awake macaque monkeys [START_REF] Fishman | Neural correlates of auditory stream segregation in primary auditory cortex of the awake monkey[END_REF][START_REF] Micheyl | Perceptual organization of tone sequences in the auditory cortex of awake macaques[END_REF] and its equivalent in the starlings' forebrain [START_REF] Bee | Primitive auditory stream segregation: a neurophysiological study in the songbird forebrain[END_REF]. A qualitatively different correlate was found using magnetoencephalography [START_REF] Gutschalk | Neuromagnetic correlates of streaming in human auditory cortex[END_REF]. The Split percepts were associated with larger longlatency potentials (P1m and N1m) for the B-tones. These potentials are thought to originate from non-primary auditory areas, the lateral Heschl's gyrus, the planum temporale, and the superior temporal gyrus. The current data on the neurophysiological bases of bistability in the visual and auditory modalities are thus consistent with a distributed competition hypothesis, although the respective contributions of the various stages remain to be elucidated.

Implications for models of auditory scene analysis

Most models of streaming are based on adaptation, starting from the auditory nerve and brainstem [START_REF] Beauvois | Computer simulation of auditory stream segregation in alternating-tone sequences[END_REF] up to auditory cortex [START_REF] Micheyl | Perceptual organization of tone sequences in the auditory cortex of awake macaques[END_REF]. Micheyl et al. [START_REF] Micheyl | Perceptual organization of tone sequences in the auditory cortex of awake macaques[END_REF] found that neural responses to ABA-sequences decrease with presentation time, but with different time constants for A and B tones. The time when responses to B-tones fell below a fixed spike-count threshold predicted accurately the average build-up of streaming observed for human subjects. Within the framework of bistability, such a multisecond-habituation mechanism could account for the specific characteristics of the first perceptual switch (Figure 1A). It would be of interest to extend the adaptation model to account for the dynamics of spontaneous alternations in the stochastic steady-state of streaming. Temporary reversals of the habituation process should then be observed. When the neural data become available, models of visual bistability that include mutual inhibition can provide inspirations to explain these dynamic effects [START_REF] Alais | Binocular Rivalry[END_REF].

Distributed or "integrated" competition at different levels of the central nervous system has recently been proposed by Cusack as a model of auditory scene analysis [START_REF] Cusack | Auditory perceptual organization inside and outside the laboratory[END_REF]. This approach can accommodate a range of behavioral and neural data, in addition to having desirable computational properties (Cusack 2005, Cognitive Neuroscience Society meeting). Here we have shown that auditory and visual bistability share many features, and that a distributed competition hypothesis is consistent with this finding. Bistability is a means to highlight mechanisms normally used to achieve stable perceptual organization. A potentially useful principle to resolve perceptual ambiguities could be the existence of competition mechanisms, based on adaptation and mutual inhibition, at multiple neural processing stages.

Experimental procedures

Auditory stimuli

The auditory stimuli consisted of 4-minute long sequences presented over headphones. A high-frequency pure tone A alternated with a low-frequency pure tone B, in an ABA-pattern. The frequency of A was 587 Hz and that of B was 440 Hz (5 semitones difference). The duration of each tone was 120 ms. The silence '-' that completed the ABA-pattern was also 120 ms long, so making the A tones isosynchronous. Listeners initially adjusted the loudness of the tones to a comfortable level which was maintained constant during the experiment.

Visual stimuli

The visual stimuli consisted of two rectangular-wave gratings presented through a 4-degree radius circular aperture. The gratings comprised thin dark stripes (duty cycle = 0.3, spatial frequency = 0.5 cycle/deg) on a lighter background, and appeared as figures moving over the background. The intersections regions were darker than the gratings (multiplicative transparency). The gratings were moving at 1.2 deg / sec in directions 120 degrees apart. A red fixation point over a 1 degree circular gray mask was added in the middle of the circular aperture and subjects were instructed to fixate this point throughout stimulus presentation.

Procedure

Observers were instructed to report their conscious perception of each stimulus continuously during stimulus presentation. They started with auditory presentation and were asked to decide whether they heard one or two streams. A third, "indeterminate" response type was available if they heard something else or were not sure about their perception at a given instant. Responses were collected via 3 buttons on a computer keyboard. A response indicated by a button press was held until a subsequent button press. In the first run, subjects were simply instructed to pay attention to the stimulus (Neutral task). In the subsequent two presentations, they were instructed to either try to hear a one-stream percept (Group task), or to try to hear a two-streams percept (Split task) in random order of presentation. Judgments with visual presentation of plaids were then performed, with an identical procedure and the three different tasks (Neutral, Group, Split). Judgments were collected continuously at a sampling rate of 20 Hz. The default response when each run started was "indeterminate".

Twenty-three observers participated in the experiment (average age: 23) with no self-reported hearing problem and normal or corrected-to-normal eyesight. They gave informed consent to participate to the experiments.

Statistical analyses

A detailed description of all statistical analyses is provided as Supplemental Data.

To check whether the switching rate between percepts was stable over time, the first 7 perceptual phases were extracted from each trial of the Neutral task. A planned comparison showed that for both the auditory and visual modalities, the first phase had a longer duration than subsequent ones. With the first phase excluded, best fitting linear trends indicated no significant drift up or down. In order to test whether the distribution of phases followed a lognormal distribution, we transformed the data from all three tasks onto a log scale and performed an analysis of variance. The distribution of residuals of the ANOVA was not statistically different from a normal distribution (Kolmogorov-Smirnov test). Distribution of normalized phases for auditory and visual stimuli in the neutral task were compared with a Kolmogorov-Smirnov test, which exhibited no significant difference. The independence of successive phase durations was assessed on the distribution of correlations between normalized log-phases, for each subject. The effects of intention were estimated on the proportion of the total time spent reporting the Grouped percept and on the average phase duration of the Split and Grouped percept after transforming phase durations to their natural logarithm and excluding the first and last percepts. Repeated measures ANOVAs were performed on theses values with the variable "task" and "modality" (Figure 2A) or "task" and "percept type" (Figure 2B,C) as independent factors. Effects of intention on the duration of percepts were estimated by post-hoc analyses.

Statistical analyses

Duration of percepts. We first checked whether the switching rate between percepts was stable over time. The first 7 percept durations were extracted from each trial of the Neutral task. This first analysis was restricted to the first 7 switches to be able to include the data from most subjects -20 subjects for streaming and 23 subjects for plaids. For both the auditory and visual modalities, the first percept had a longer duration than subsequent phases (planned comparison Aud. F(1,133)=14.8, p<10 -3 , Vis. F(1,154)=40.4, p<10 -8 ). With the first phase excluded, best fitting linear trends indicated no significant drift up or down. Correlation coefficients were calculated on log durations (see [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF] for details). Aud. percepts: r = 0.02 p = .84; Vis. percepts: r = 0.13, p = .12. Similar results can be obtained when including more percepts, see Figure S2, Additional subjects with repeated measures.

Test of lognormal distribution. In order to characterize the distribution of percept durations, a large number of observations is needed. These observations are obtained with different observers in different runs. This brings variability into the data which is not related to the nature of the distribution of percept durations per se. For instance, if the data of a fast switcher are aggregated with those of a slow switcher, a bimodal distribution is obtained. Most investigators of bistability use "normalized" distributions to correct for this variability, that is they divide all phase durations by the average duration for each experimental run. This is how we obtained the data presented in Figure 1C,D.

While this method is useful to illustrate the shape of the distribution, it is statistically questionable when dealing with strongly asymmetrical distributions like the gamma or lognormal distribution. The "mean" is very different from the mode and the median of the distribution and its exact value strongly depends on the presence of extreme values. A more rigorous way of testing the shapes of distributions is the indirect method proposed by Hupé and Rubin [START_REF] Hupé | The dynamics of bi-stable alternation in ambiguous motion displays: a fresh look at plaids[END_REF]. In order to test whether the distribution of phases followed a lognormal distribution, we transformed the data onto a log scale (natural log of durations)

and performed an analysis of variance. For this analysis, we pooled together the results

for the three different tasks on a given modality in order to increase the power of the statistical test. The analysis was performed with subjects as a random factor, task and percept as fixed factors, and interactions were taken into account. The distributions of residuals of the ANOVAs were not statistically different from a normal distribution, validating the log transformation and showing that the original distributions were indeed lognormal (Tables S1,S2, Figure S3).

Independence between successive durations. Figure 1 E, F indicates that, overall, there is no strong correlation between successive phase durations. The data points, however, pools together observers with different switching rates (Fig. 3A) and proportion of time spent in the Grouped percept that were not always 50% (Fig. 3B). In order to handle inter-individual differences, correlation coefficients between successive durations were computed for each subject. t. Phase durations were transformed to their natural logarithm. The first and last percepts were excluded, as the first one is longer that the others (Figure 1A,B) and the last one was interrupted by the end of the stimulus presentation. Phase durations were then normalized: each log duration was divided by the mean of the log durations for each run and each percept type. Mean r values (and standard deviations) across the population were: r=0.13 (0.20) for auditory bistability and r=0.08 (0.16) for visual bistability. These values were not significantly different from zero (Aud.: p = 0.12, Vis.: p = 0.10, Non-Parametric Sign test). We also found no significant correlation when testing independently each transition type (from Split to Group and from Group to Split), nor when testing possible correlations between a given Group (or Split) epoch and the next Group (or Split) epoch [START_REF] Rubin | Dynamics of perceptual bi-stability: plaids and binocular rivalry compared[END_REF].

Effects of intention. Different measures were computed for each 4-minute run: the proportion of the total time spent reporting the Grouped percept, and the average phase duration of the Split and Grouped percepts. The first and last percepts were discarded, which led to exclude from these group analyses 3 subjects who had experienced less than three percepts in one of the conditions. Phase durations were transformed to their natural logarithm. Repeated measures ANOVAs were performed on theses values, with the variable "task" and "modality" (Figure 2A) or "task" and "percept type" (Figure 2B,C) as independent factors. The ANOVA tables are presented in Tables S3, S4 and S5.

The effects of intention on the duration of percepts were estimated by post-hoc analyses. Intention shortened the unwanted percept mean duration: Aud. Group task vs.

Neutral, p = 0.002 for the Split percept; Aud. Split task vs. Neutral, p = 0.001 for the

Figure 1

 1 Figure 1 Temporal dynamics for auditory and visual bistability. (A, B)The durations of the first seven successive phases are presented for both the auditory modality (A, dark grey) and the visual modality (B, light grey). Durations were first transformed to a log scale, then averaged across all participants that experienced 7 or more successive phases (Audition N=20, Vision N=23). The error bars represent 95% confidence intervals around the mean estimated by 1.96 standard error. The logscale is converted back to seconds for display purposes. The first percept is significantly longer that subsequent ones. There is no long-term trend in the duration of phases after the first one. (C, D) The histograms of durations of Grouped and Split phases are presented, compiled for all participants (N=23) and percept types (Grouped and Split). All durations were normalized by the average phase duration in each given run. The first phase was excluded from the analysis as it lasted longer than subsequent ones. There is no significant difference between the distributions for the two modalities (Kolmogorov-Smirnov test, p=0.1). (E, F) The duration of a percept is shown as a function of the duration of the previous percept, for all participants (N=23). These are the same data that constitute the histograms of panels C, D, but in raw format without any normalization. The duration of a phase does not influence the duration of the next phase, for both modalities. All data in this figure from the Neutral task.

Figure 3

 3 Figure 3 Absence of correlation between subject-specific measures across modalities. (A) The number of perceptual switches in the visual modality is plotted as a function of the number of switches in the auditory modality, for the Neutral task. Each point represents an individual observer (N=23). The number of switches is not correlated across modalities. (B) The relative amount of time where the stimuli are perceived as Grouped is compared for both modalities, for each individual observer, in the Neutral task. There is no idiosyncratic tendency to favor a Grouped or Split interpretation across modalities. (C) The magnitude of the effect of volitional control is compared across modalities. The effect was quantified by subtracting the proportion of Grouped percepts between the Group and Split intentions, for each observer. The magnitude of the effect of volitional control is uncorrelated across modalities.

Figure S2 .

 S2 Figure S2. The duration of successive percepts in auditory streaming is stable over time. The duration of successive (A) Grouped phases and (B) Split phases is shown for the new group of 7 participants and 6 repeats. Individual points are the raw values for all experimental runs. Horizontal bars represent the mean of log-durations. Regression lines fitted to the successive phases, except for the first Grouped phase, show no long-term trend in the duration of percepts.

Acknowledgments

The authors would like to thank Christophe Micheyl, Rhodri Cusack, Jan Schnupp, and Alain de Cheveigné for useful comments on previous versions of this manuscript.

Supplemental data

Stimuli

Error 4084