F Suchanek

A Bozzon

E Della Valle

A Campi

S Ronchi

Towards an Ontological Representation of Services in Search Computing

 to represent Web Services in conjunction with YAGO. We draw parallels to the Service Mart [3] model used in SeCo. We propose a symbiosis of the two models, discussing the challenges and advantages that come with the integrated model.

Introduction

The Search Computing project (SeCo) [START_REF] Ceri | Search Computing[END_REF] uses the Semantic Resource Framework (SRF) to model Web services. The SRF is a multi-layer model. The higher layers provide an abstract semantic description of the services, building on the notions of Service Marts and Connection Patterns. The lower layers (service interfaces and access patterns) are concerned with the physical properties of the services. Ideally, every service belongs conceptually to a Service Mart. A Service Mart is structurally defined by means of attributes. Two Service Marts can be connected by a Connection Pattern. At the logical level, each Service Mart is associated with one or more access patterns representing the signatures of the service calls. Access patterns contain a subset of the attributes of the Service Mart, which are tagged with either I (input), or O (output). Attributes can also be tagged as R (ranking), to denote attributes that are used for ordering result instances. Ranking is particularly important in SeCo, because it allows mastering the combinatory explosion of multi-domain queries typical in Search Computing.

By design, the creation of a SRF is a bottom-up process, whereby the real world entities modeled by the Service Marts are typically created on the basis of the Web services. In this article, we try to anticipate how SeCo can cope with a large scale deployment scenario with a larger number of administrators and services. We argue that, when the complexity of the knowledge represented in a SeCo deployment increases, the SRF model might benefit from adapting ideas from the Semantic Web technologies. Therefore, we propose to substitute the topmost level of the SRF (the service marts) with an ontology. We argue that this will reduce the maintenance effort for a SRF with a large number of data sources, and facilitate the interaction of SeCo with ontology-based systems.

In order to motivate why the SRF model used in SeCo may need to be extended with an ontological representation, we start with a example.

Motivation

The SRF model leaves room for modeling the same data source in different ways. Assume for example the availability of two search services (Figure 1). The first, ws 1 , exposes information about movies played in theaters located close to a given location. The second service, ws 2 , queries a repository containing information about movies. The access patterns of these two Web Services can be described on the conceptual level of the SRF as two service marts MOVIE and THEATRE (see Figure 2), where the attribute Movie of the service mart THEATRE is linked to the attribute Title of the service mart MOVIE .

WS1 WS2

Fig. 1. The Access Patterns for ws1 and ws2 on the logical level.

THEATRE Name Address Movie

MOVIE

Title Year Cast

Actor Role Projection Fig. 2. Two service marts for ws1 and ws2 on the conceptual level. Now let's assume the availability of a service ws 3 , which, given a place, searches for all the actor s that were born there and returns a description of the actor, including the list of the movies he played in (Figure 3). As we explained in the introduction, ideally, each service belongs to one Service Mart. The service ws 3 does not belong to any of the service marts that have already been defined. Therefore, the SRF administrator is confronted with two If there are multiple SRF administrators, different SRF administrators may choose different (and potentially redundant or incompatible) modeling approaches. In the case of a large scale deployment of a Search Computing system, with potentially hundreds of services and dozens of administrators, these small incompatibilities may quickly add up, leaving the SRF model cluttered with redundancies and inconsistencies. These inconsistencies can lead to major maintenance problems once the size of the SRF surpasses what a single human can assess.

Contribution

In this chapter, we propose an evolution of the SRF knowledge representation model that will allow it to cope better with some of the maintenance challenges described above. Our proposed model leverages the ontological model that is used in the Semantic Web. It builds on ANGIE [START_REF] Preda | Active knowledge: Dynamically enriching rdf knowledge bases by web services (angie)[END_REF], a novel approach for Web service description based on the YAGO Ontology [START_REF] Suchanek | Yago: A Core of Semantic Knowledge[END_REF]. We show that our proposed model not only eases the problem of design alternatives, but also brings additional benefits for the maintenance of the SRF. The new model does not come without challenges of its own. Therefore, this chapter pursues a rather inspirational goal, laying the ground for further investigation.

The chapter is structured as follows: Section 2 discusses the related work; in Section 3, we present YAGO and ANGIE. In Section 4, we propose a merger of the ANGIE knowledge representation model and the SeCo model. In Section 5 we elaborate on the properties of our proposed hybrid model. Finally Section 6 discusses potential future work and concludes.

The combination of ontologies and services has been proposed before [START_REF] Mcilraith | Semantic web services[END_REF][START_REF] Preda | Active knowledge: Dynamically enriching rdf knowledge bases by web services (angie)[END_REF][START_REF] Sivashanmugam | Adding semantics to web services standards[END_REF]. The ultimate goal of such an endeavor is to enable a higher degree of automation for the tasks involved in the life-cycle of service based applications. These include (among others) the discovery and selection of services, their composition, their execution and their monitoring. As proposed first in [START_REF] Sivashanmugam | Adding semantics to web services standards[END_REF], ontologies can be used to model four types of service semantics: data semantics (the semantics pertaining to the data contained in the data source), functional semantics (the semantics pertaining to the functional capabilities of the service), non-functional semantics (the semantics related to the non-functional aspects of the service, such as security or reliability) and execution semantics (the semantics related to the invocation, result processing and exception handling of the service).

Several ontology have been proposed to describe these semantics and annotate services. The most well-known ones are OWL-S [START_REF] Burstein | Owl-s: Semantic markup for web services[END_REF], WSMO [START_REF] Fensel | Enabling Semantic Web Services: The Web Service Modeling Ontology[END_REF], SAWSDL [START_REF] Farrell | Semantic annotations for wsdl and xml schema[END_REF] and WSMO Lite [START_REF] Vitvar | Wsmo-lite annotations for web services[END_REF]. Some of them hypothesized the need to semantically describe services at a level of detail that even requires to define a specific ontological language, e.g., the Web Service Modeling Language [START_REF] De Bruijn | Modeling Semantic Web Services: The Web Service Modeling Language[END_REF]. All these existing approaches have been perceived unsuited by practitioners in large scale deployments; mostly because of the extra cost of annotating services.

To avoid this pitfall, we decided to look for a light weight approach possibly based on a minimal ontological language. Therefore, we turn our interest to ANGIE [START_REF] Preda | Active knowledge: Dynamically enriching rdf knowledge bases by web services (angie)[END_REF], a novel approach that is centered on YAGO Ontology [START_REF] Suchanek | Yago: A Core of Semantic Knowledge[END_REF]. ANGIE leverages the "lightest" of the ontological languages, RDF. This model builds only on typed resources and labeled links. ANGIE uses RDF to describe the input and the output parameters of Web Services and to orchestrate their invocation in order to dynamically extend YAGO with instances loaded from the Web. In the remainder of the chapter we report our initial findings on how ideas from the ANGIE model can ease the definition of new services in SeCo.

YAGO and ANGIE

YAGO

YAGO [START_REF] Suchanek | Yago: A Core of Semantic Knowledge[END_REF] is a large semantic knowledge base (an ontology). It contains 3 millions entities (such as movies, cities, universities and people) and 28 millions facts about them (such as birth dates, appearances in movies, geographical location etc.). YAGO was constructed automatically from Wikipedia and WordNet [START_REF] Fellbaum | WordNet: An Electronic Lexical Database[END_REF]. In YAGO, knowledge is represented in the RDFS model [START_REF] Consortium | Rdf primer, w3c recommendation[END_REF]. This model can be seen as a directed labeled multi-graph, in which nodes represent entities and edges represent relationships between the entities. For example, the node Apollo Theatre is linked to the node Shall we dance by an edge labeled shows (see Figure 5). The labels of the edges are called relations. YAGO uses a set of 100 predefined relations. These include a variety of link types, such as bornIn, locatedIn, directedMovie or isCapitalOf. RDF knowledge bases distinguish between instances (such as Jennifer Lopez, drawn thin) and concepts, i.e., groups of similar instances (such as actor or movie, in bold). Instances and concepts are both nodes in the RDF graph. For example, the concept movie is a node in the RDF graph. An instance is linked to its concept by the relation type. A concept is linked to a more general concept by the relation subclassOf. For example, the sub-concept actor is linked to the super-concept person in this way. Whenever an instance is an instance of a subconcept, it is automatically an instance of all of its super-concepts.

!"#$%&#' ()*+#' ,-%)&' .#&/)0' 12+34+05' 6#00+7#&' 8)9#:' ;"$33'<#' =$0-#' ,9)33)' !"#$%&#' %>9#' %>9#' %>9#' /2?-3$//@7' /2?-3$//@7' /")A/' /")A/' B)3#' B#/%$2&$0%' 8)-$C)0' 3)-$%#4,%' 93$>/' .$23+0$' 93$>/' %>9#' "$/' "$/' !#&D+0)3)5>' ,//#&C)0/' =+/%$0-#' 4+/%'
Relations are by themselves nodes in the RDF model. This makes it possible to talk about properties of relations in the same way as about instances. For example, to say that the domain of shows is the concept theatre, we can link the node of shows to the node theatre by the relation hasDomain (not shown in the figure). For illustration, we draw the relations as dashed arrows between the domain concept and the range concept (as shown in Figure 5). Every instance of a sub-concept of theatre (e.g., every instance of 3d-theatre) is also an instance of theatre. Thereby, the relation shows applies automatically to all instances that live somewhere below the concept theatre.

Different from classical database models, RDF models are inherently schemaless. This means that any instance can be linked to any other instance with any relation, as long as the domain and the range constraint of the relation are not violated.

ANGIE

ANGIE [START_REF] Preda | Active knowledge: Dynamically enriching rdf knowledge bases by web services (angie)[END_REF] is a system that uses Web services to extend YAGO. ANGIE requires the manual registration of Web service and a manual mapping of the input and the output of the services to the concepts of the ontology 3 . Once the Web services have been registered, ANGIE allows answering queries on the knowledge base. Whenever the data in the knowledge base is not sufficient to answer a query, ANGIE calls the Web services to retrieve the required additional information. ANGIE can automatically determine the Web services that have to be called to answer the query and it can automatically combine different Web services should that be necessary. This process is transparent to the user, so that the user has the impression of browsing a huge knowledge graph -even though this graph is extended on the fly behind the scenes with the data from the Web services. While ANGIE can deal with arbitrarily-shaped Web services, it cannot deal with ranking of the results.

ANGIE works on conjunctive SPARQL queries. These queries can be thought of as RDF graphs that may have variables in the place of the nodes. For example, a user may ask for all movies of the Apollo Theatre by the query depicted in Figure 6. An answer to such a query is a subgraph of the ontology that is isomorphic to the query. In the example, we can match the query on the ontology depicted in Figure 5 with ?m =Shall we dance. Therefore, ?m =Shall we dance is an answer to the query.

Web Service Orchestration If a query cannot be matched on the ontology, or if we want to retrieve more answers than the ontology knows, ANGIE can resort to Web services. A Web service is represented just like a query: as an RDF graph that can contain variables in the place of nodes. Each edge is either an input edge or an output edge. Figure 6 shows a Web service at the top right, which requires as input (solid) a variable ?a that must be an theatre and delivers as output (dashed) a fact that the theatre shows some movie ?b and that ?b is a movie. Before the Web service can be called, all variables in the input edges have to be instantiated. When the Web service returns its results, these are instantiations of the variables in the output edges.

When ANGIE receives a query, it tries to cover the query graph with (1) edges from the ontology or (2) output edges of Web services. Consider the example in Figure 6. We start with the query at the bottom. We cover the query with an instantiation of the Web service (on the layer above). The Web service covers the query edge (solid) with an output edge (dashed). It introduces an additional output edge (that ?m is of type movie, dashed), which we did not ask for. It also introduces an input edge (that the Apollo Theatre has to be a theatre, solid). Now, the procedure is repeated: Every input edge has to covered again, either by the output edge of another Web service or by an edge from the ontology. In the example, the fact that the Apollo Theatre is a theatre is already in the ontology. Therefore, we can cover this input edge (solid) with the edge from the ontology (top layer, dashed). Now, every input edge and the query is covered. If we call the Web services from top to bottom, we will receive answers to the query. In our example, there is only one Web service, but if there are that provide information about a give topic or entity, and part of the execution semantics, since it describes input and output, but cannot handle exceptions. No formal description of the non-functional semantics is provided. multiple Web services, then the outputs of one service are "piped" into the inputs of another service. ANGIE implements a sophisticated scheduling algorithm that can compute such query covers efficiently and give preference to covers that are likely to return more answers. This works even when the query covers are recursive.

All data retrieved from the Web services is added to the ontology. Thereby, future queries can make use of the knowledge that has already been computed.

Virtual Web Services In some cases, the way the ontology models the data and the way the Web services return the data may not coincide. Consider for example the Web services depicted in Figure 7. While the first Web service can return the actors for a given movie, the second service can return not only the actors but also their roles. If the user asks only for the movies (as in the figure), Web service 1 can be applied, but Web service 2 cannot, because none of its output edges matches the query. Even the edges from the ontology cannot be applied, since the ontology models roles as a separate entity.

To bridge such mismatches, ANGIE supports virtual services. A virtual service is a pseudo Web service that does not have a physical Internet service behind it. "Calling a virtual service" means matching the input edges and then adding the output edges to the query cover -without any physical Web service call. In the example in Figure 7, the virtual service allows adding a playsIn fact, if there are plays and has facts for a role.

With the virtual service, our query can be answered even with Web service 2: We first call Web service 2 to retrieve movies together with their roles. Then, we "call" the virtual Web service to transform the output into playsIn facts that answer the query. Such a call does not involve any physical Web service call. It is a pure data manipulation on the query edges, which allows us to bridge data modelizations of different granularity.

Toward an ontological representation of the access patterns

Inspired by the ANGIE approach, we propose to substitute the Service Mart layer of the SRF model with the YAGO ontology. The role of Service Marts will be taken over by the concepts and relations of the ontology -just like explained in Section 3.2. Thereby, the conceptual layer of the SRF for the running example will be the ontology depicted in Figure 5.

In addition, we propose to describe the access patterns in the way Web Services are described in ANGIE: Each access pattern becomes a graph. The edges are labeled with relationships from the ontology. The nodes can be either constants from the ontology or variables. Each attribute of an access pattern becomes an edge that is labeled with the corresponding relationship from the ontology. This edge connects to a node with a variable. Structured attributes become star-shaped patterns. As in ANGIE, nodes are labeled as input nodes or output nodes. The type of a variable node is indicated by an outgoing type edge to a concept node.

To cope with the notion of ranking (typical for SeCo), ANGIE's representation of Web services has to be extended so as to allow not only input nodes and output nodes, but also ranking nodes. In every access pattern graph, there can be at most one node that is labeled as a ranking node. Such a node has to be an output node. In the illustrations, we represent a ranking node by a filled dashed frame. Figure 8 shows how the access patterns ws 1 and ws 2 from the introduction can be modeled; ws 1 , which belonged to the Service Mart Theater, requires as input (solid) a variable ?a, a location, and produces as output (dashed) the theaters ?c, located at a distance ?b from the input location, and showing some movie ?d; the results of ws 1 are also ordered according to the distances ?b. Likewise, ws 2 , which belonged to the Service Mart Movie, requires as input a the title ?e of movie ?a, and it produces as output the actors ?d that acted in the movies with the role ?c; results are ordered according to the production year ?b.

Noteworthily, the novel RDF representation is isomorphic w.r.t. the original one. This assures compatibility with the service description exploited by the other levels of the architecture. Indeed, we remark that all of our proposed changes happen purely at the level of service modeling. No changes to the Web service composition algorithms or the ranking algorithms of SeCo are necessary.

Properties of the Proposed Model

We note that the proposed representation helps in coping with the issues mentioned in the introduction: as Figure 9 depicts, there is no ambiguity whether the information brought by ws 3 shall be stored within the service mart MOVIE or ACTOR. The administrator just has to describe the access pattern as a query on YAGO ontology: the access pattern selects instances of actors (?a type Actor) based on their birthplace (?a bornIn ?b), ranked by the date of birth (?a bornWhen ?e) and lists the movies they played in (?d type Movie; ?a plays ?c; ?d has ?c).

Given that every concept and property exists exactly once, there are fewer possibilities for inconsistencies to appear in the ontological model. In addition to the specific maintenance case that we developed through the paper, the use of an ontological description for the conceptual level brings several advantages: notably, the ontology can evolve independently from the registered data sources. In the SRF model that we are proposing, the ontology models the world and the access patterns model the Web Services. An extension of the ontology will not influence the access patterns. For instance, the subclass Restaurant of Building can exist in the ontology even if no access pattern refers to it. Vice versa, the addition or removal of an access pattern will not influence the ontology (provided that all necessary relations and concepts are present). Thereby, the roles of the ontology and the access patterns are clearly defined and distinct.

Since the ontology allows for the creation of sub-concepts, more specific concepts can be created without having to redo the work that has been done for the super-concept. The attributes of the sub-concept are automatically consistent with the attributes of the super-concept. By design, a Web service that delivers an instance of the sub-concept can also be used to deliver an instance of the super-concept. Furthermore, through the domains and ranges of relations, the target type of a relation is explicitly defined. There is no need to replicate this information with every link or every Web service. Target types are an inherent part of the model.

Since relations are first-class citizens of the model, the joinability of attributes follows directly from the definition of the relations and the access patterns. For example, if a Web service returns movies, then the joinability with another Web service that returns movies follows from the fact that both output variables are of type movie. This also works across different levels in the concept hierarchy: If one Web service returns 3d-movies and the other Web service returns silent movies, these Web services are still joinable, since both concepts are sub-concepts of movie. By factoring out this common information from the level of Web services to the level of classes, the ontological model avoids redundancy.

The only maintenance task left to SRM administrators is the extension of the ontology when the registration of a new Web Service requires adding new concepts and relationships to YAGO. For instance, if the relationship bornIn is not present in the ontology, but is brought in by a Web service, then this relationship has to be added by the SRF administrator. This is not a trivial task per se, but at least we can rely on established methodological approaches (e.g., METHONTOLOGY [START_REF] Corcho | Building legal ontologies with methontology and webode[END_REF], On-To-Knowledge [START_REF] Sure | Methodology for development and employment of ontology based knowledge management applications[END_REF], and DILIGENT [START_REF] Pinto | Diligent: Towards a fine-grained methodology for distributed, loosely-controlled and evolving engineering of ontologies[END_REF]) for ontology development and maintenance.

Conclusions and Future Work

In this article, we have discussed some of the maintenance challenges that SeCo will face when more users, services and administrators start using the system in parallel. We have argued that, for this task, the SeCo knowledge representation model would benefit from a more ontological design. We have proposed and studied an ontological adaptation of the SeCo model, inspired by the model used in the ANGIE system. We have shown that the new model mitigates some of the maintenance challenges, thus contributing to SeCo's fitness for going mainstream.

We believe that, apart from easing some of the maintenance challenges, an ontological top layer of SeCo opens the door to a wide range of possible interactions between SeCo and existing ontologies. These include not only YAGO but also the vast resources of the Linking Open Data Project (LOD) [START_REF] Bizer | Linked data -the story so far[END_REF]. Whilst the LOD has not been the focus of this article, we are confident that the shared knowledge representation will ease knowledge exchange between the LOD and SeCo in the future -e.g., by answering queries with data from the LOD in case a Web service is not available.

We believe that there is much further research potential in the combination of ANGIE and SeCo. For example, the orchestration algorithm of ANGIE can only combine the outputs of one Web Service with the inputs of another Web Service (i.e., it can only perform pipe joins, in SeCo terminology). Therefore, some registered Web Service cannot be used directly. SeCo, in contrast, can master the combinatory explosion that appears when results from multiple Web Services are combined, because it uses rank aware parallel join operators.

On the other hand, ANGIE is very good at answering SPARQL queries. This is an avenue on which SeCo could benefit. One possibility to combine the advantages of SeCo and ANGIE would be to register Web Services both in ANGIE and in SeCo. Whenever a user issues a SPARQL query on YAGO, ANGIE could orchestrate (virtual and real) Web Services normally whenever it can pipe the output of one Web Service into the input of another Web Service. When ANGIE faces the problem to perform parallel joins on the results of multiple Web Services, it could delegate the execution of this part of the orchestration to SeCo. This is just one example for the research possibilities that wait to be discovered in further cross-fertilization of these approaches.

Fig. 3 .

 3 Fig. 3. The Access Pattern for ws3.

Fig. 4 .

 4 Fig. 4. Examples of alternative evolution of the service marts

Fig. 5 .

 5 Fig. 5. An excerpt from an RDF ontology.

Fig. 6 .

 6 Fig. 6. A user query, a Web service, and a query cover.

Fig. 7 .

 7 Fig. 7. A virtual Web service.

  locatedAt

Fig. 8 .

 8 Fig. 8. RDF representation of two Access Patterns shown in Figure 3.

Fig. 9 .

 9 Fig. 9. The Web service ws3 in the new model.

  ). Since structured attributes can replicate the attributes of other concepts, both options are valid and none of them is a priori better than the other.

	MOVIE			ACTOR
	Title Year	Cast	Name Birthdate	Birthplace	Plays
	Actor Role Birthdate Birthplace			Movie Role

Such a mapping captures in a very light-weight way the data semantics, since all data types exchanged with the Web Service are mapped to ontological concepts. It also captures part of the functional semantics, since ANGIE can only model Web Services

⋆⋆ The work by Fabian Suchanek has been partially funded by the European Research Council under the European Community's Seventh Framework Programme (FP7/2007-2013) / ERC grant Webdam, agreement 226513. http://webdam.inria.fr/


Jean-Yves Marion

A type system for complexity flow analysis

We propose a type system for an imperative programming language, which certifies program time bounds. This type system is based on secure flow information analysis. Each program variable has a level and we prevent information from flowing from low level to higher level variables. We also introduce a downgrading mechanism in order to delineate a broader class of programs. Thus, we propose a relation between security-typed language and implicit computational complexity. We establish a characterization of the class of polynomial time functions.

I. INTRODUCTION

This paper introduces a new static analysis method for controlling and certifying imperative program runtime. We propose a type system to reflect information flow and to explore the computational complexity properties of well-typed programs. We exhibit a relation between Implicit Computational Complexity approaches and research on language-based information flow security.

The subject of Implicit Computational Complexity (ICC) is the characterization of complexity classes without referring to machines and so with no externally imposed resource bounds on time or space. Early examples of implicit characterization of PTIME are via bounded recursion by Cobham [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF], fixpoint logic by Immerman [START_REF] Immerman | Relational queries computable in polynomial time[END_REF], positive-existential comprehension in second-order logic by Leivant [START_REF] Leivant | Predicative recurrence and computational complexity i: Word recurrence and poly-time[END_REF], safe recursion by Bellantoni & Cook [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF], ramified recursion by Leivant [START_REF] Leivant | A foundational delineation of poly-time[END_REF], restricted lambda-calculi by Leivant & Marion [START_REF] Leivant | Lambda calculus characterizations of poly-time[END_REF], light linear logic by Girard [START_REF] Girard | Light linear logic[END_REF] and Lafont [START_REF] Lafont | Soft linear logic and polynomial time[END_REF], linear types by Hofmann [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF], and syntactically restricted induction [START_REF] Marion | Actual arithmetic and feasibility[END_REF], to mention a few.

Since Bell & La Padula [START_REF] Bell | Secure computer system: unified exposition and multics interpretation[END_REF] and Biba [START_REF] Biba | Integrity considerations for secure computer systems[END_REF], secure information flow uses a lattice of security levels to ensure confidentiality and integrity. Each variable is assigned a security level. The type system guarantees the security policy induced by the lattice. An important property, called non-interference [START_REF] Goguen | Security policies and security models[END_REF], consists in demonstrating that values of high level variables are independent from values of low level variables during a program execution. The use of type systems in this context was pioneered by Volpano, Smith and Irvine [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. Type systems for secure information flow were investigated extensively see e.g. Sabelfeld and Myers survey [START_REF] Sabelfeld | Language-based information-flow security[END_REF].

Another important issue is declassification. Sometimes it is necessary to release information, which is usually done by downgrading the security level of variables. In the context of integrity, declassification is also called endorsement. For a comprehensive survey, see the article by Sabelfeld and Sands [START_REF] Sabelfeld | Declassification: Dimensions and principles[END_REF] .

Related works

There are several works related to ICC on resource analysis for imperative programming language. In [START_REF] Jones | The expressive power of higher-order types or, life without cons[END_REF] Jones characterizes PTIME by means of simple constructor free programs. Data flow analysis to bound variables growth rate is performed by matrix calculus in Jones & Kristiansen [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF], Niggl & Wunderlich [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF], and Ben-Amram, Jones & Kristiansen [START_REF] Ben-Amram | Linear, polynomial or exponential? complexity inference in polynomial time[END_REF]. However the language is restricted to loops of fixed length, and operators are successor-like functions. Finally, Marion & Péchoux [START_REF] Marion | Analyzing the implicit computational complexity of object-oriented programs[END_REF] extend interpretation methods [START_REF] Marion | Efficient first order functional program interpreter with time bound certifications[END_REF] to object oriented languages.

There are other recent approaches to compute resource consumption bounds. Jost, Hammond, Loidl & Hofmann [START_REF] Jost | Static determination of quantitative resource usage for higher-order programs[END_REF] work on automatic amortized cost analysis using type systems, which is related to the study of non-size increasing systems. Hughes, Pareto & Sabry [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF] propose sized types in order to determine bound on data structure sizes. Albert, Alonso, Arenas, Genaim, & Puebla [START_REF] Albert | Asymptotic resource usage bounds[END_REF] design cost analyser for java byte codes. Lastly, the approach of Gulwani, Mehra & Chilimbi [START_REF] Gulwani | Speed: precise and efficient static estimation of program computational complexity[END_REF] consists in automatically finding loop invariants and is related to abstract interpretation methods.

Contributions

We present a type system for an imperative programming language over words. Programs are built from while loops and expressions are built from predicates, constructor and destructor operators. To control the size of the information flow, the type system is based on a complexity lattice. Each variable is assigned a type, which is a pair of tiers, i.e. elements of the complexity lattice. There is a declassification mechanism, which allows applying safely operators inside loops. We demonstrate that the type system is sound with respect to a timed structural operational semantics. For this, we establish first a non-interference result, which shows that values of higher tier variables do not depend on values of lower tier variables. Then, we show that a consequence is a theorem of temporal non-interference: the length of loops depends only on values of higher tier variables. Another consequence is a weak polynomial time termination procedure. Finally, we demonstrate that terminating and well-typed programs are computable in polynomial time over the two tier lattice ({0, 1}, , 0). Conversely, each polynomial time function is implemented by a well-typed program.

Informal motivation

We give an informal presentation of the main ideas behind a type system for complexity flow analysis. Our point of departure is the definition of functions by ramified recursion as suggested by Leivant in [START_REF] Leivant | A foundational delineation of poly-time[END_REF] and in essence in [START_REF] Leivant | A foundational delineation of computational feasiblity[END_REF] twenty years ago. As a result, some kinds of circular definitions are not allowed. This underlying concept of circularity is one of the most important in implicit computational complexity. Thus, Simmons [START_REF] Simmons | The realm of primitive recursion[END_REF] proposed a fine-grained study of diagonalisation to delineate primitive recursion definitions from multiple recursive definitions. His work is extended in [START_REF] Marion | On tiered small jump operators[END_REF] to show how an Ackermann style construction may be used to diagonalise away from the class of polynomial time functions. Another illustration is given by Light Linear Logic in which modalities are essential in order to prevent circular definitions, as Girard explains it in his seminal work [START_REF] Girard | Light linear logic[END_REF] . It is a guideline in order to define an information flow typing to control complexity of a simple imperative programming language. What we have in mind is to get inspiration from security-type systems like the one of Volpano, Smith and Irvine [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. A type system is defined with respect to a security policy, which specifies the use of data. Each variable is assigned a security type. Let us examine a typing rule which expresses by subtyping an explicit downward flow from E to X :

Γ X : η Γ E : ζ η ≤ ζ Γ X :=E : ζ
There is a data flow from type ζ to η, which corresponds to the no-read-down-rule of Biba's integrity policy [START_REF] Biba | Integrity considerations for secure computer systems[END_REF]. The converse should not be possible. There are implicit information flows in while-loop, which should also be controlled. Consider the following program which copies the value of the variable X into Y :

Y :=0 ; w h i l e ( X > 0 ) { X :=X -1 ; Y :=Y + 1 ; }
Here, the variable X controls the while loop. In order to bound the complexity data flow, we should require that the level of Y is strictly less than the one of X . Otherwise, a circular data flow is created, which violates the ICC concept of dataramification principle by allowing an upward flow. So, the typing rule of a while-command looks like

Γ, ∆ E : ζ Γ, ∆ C : η η ≺ ζ Γ, ∆ while(E ){C } : η
On the one hand, the guard E is of level ζ. This implies that X is also of level ζ. On the other hand, the block of commands X :=X -1; Y :=Y + 1; is of type η and η ≺ ζ. Therefore, we have to downgrade or to declassify X in such a way that the command X :=X -1 is of type η.

In order to deal with declassification, we must extend the assignment of single level tags to expressions and to commands. From now on, the type of an expression or of a command is a pair (α, β) of tiers. Roughly speaking, α is the starting level. β indicates that the information is allowed to flow down to level β. An expression E of type (α, β) is downgraded if β ≺ α. A downgraded expression may be safely assigned in a loop of tier α if β ≺ α. Since the runtime is controlled within a polynomial bound, variable and operator typing rules control the declassification process. Thus, we can only apply neutral operators to a declassified expression. We call an operator neutral if it does not increase the size of a value, as in X -1. On the other hand, some operators (called positive operators) reclassify an expression because they are unsafe in a loop, like X + 1. We have informally and briefly presented ideas that we are now describing in a more formal way.

II. A COMPLEXITY FLOW TYPE SYSTEM

A. Syntax of expressions and commands

We consider a simple imperative programming language. The syntax of expressions is given by the grammar E 1 , . . . , E n ∈ Exp ::= X | op(E 1 , . . . , E n ) where X is a variable from a set V, and op is a n-ary operator from a set O. Constants are 0-ary operators. The set of variables in the expression E is denoted V(E ). The grammar of commands is

C , C ∈ Cmd ::= X :=E | while(E ){C } | if E then C else C | C ; C We denote by |E | (|C |) the size of an expression E (resp. of a command C ).

B. Complexity lattices

A complexity lattice is a finite lattice (SC, , 0) where is a quasi-ordering on SC, 0 is the least element with respect to SC, such that for any two elements α and β, there is a unique greatest lower bound α ∧ β and a unique least upper bound α ∨ β w.r.t. . Elements of SC are also dubbed tier, for which we use discourse variables α, β, . . . In particular, we shall focus on the two tier lattice ({0, 1}, , 0). We posit a fixed complexity lattice (SC, , 0), which is implicit in the rest of this paper.

C. Expression types

The type of an expression is a pair (α, β) of tiers α, β ∈ SC. The typing derivation system is determined by the typing rules in Figure 1 and two typing environments: (i) a variable typing environment Γ : V → SC, which assigns to each variable a single tier, and (ii) an operator typing environment ∆, which is a relation that associates to each operator one or several operator types. The grammar of operator types is the following:

ρ ∈ Operator types ::= (α, β) | (α, β) → ρ
We write dom(Γ) (resp. dom(∆)) to mean the set of variables typed by Γ (resp. the set of operators typed by ∆). Lastly, we occasionally omit parenthesis using right associativity of →.

Variable

Γ(X ) = α where β α Γ, ∆ X : (α, β) Op Γ, ∆ E 1 : (α 1 , β 1 ) . . . Γ, ∆ E n : (α n , β n ) Γ, ∆ op(E 1 , . . . , E n ) : (α, β)
where

(α 1 , β 1 ) → . . . → (α n , β n ) → (α, β) ∈ ∆(op)

D. Command types

Figure 2 gives the typing rules for commands. As we shall see later, any program that is well-typed according to these rules satisfies non-interference properties as well as the ramification conditions of the ICC tiering discipline. The typing rules control information in way, which is related to Volpano, Irvine and Smith's system [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. A typing judgement is of the form Γ, ∆ C : (α, β), and means that the command C is of type (α, β), where α and β are tiers of SC, under Γ and ∆.

III. A TIMED BIG STEP SEMANTICS

We present a big step semantics, which takes the computation time into account. In an imperative language, a computation is a sequence of transition steps where at each step corresponds a store update. A transition performs a fixed number of basic operations or tests, which are counted as a unit cost. So, it is reasonable to define a time measure which corresponds to the number of transition steps.

Let W be the set of words over a finite alphabet. Expressions, commands and programs are interpreted over W. We take two words tt and ff of W to denote respectively true and false. A store µ is a finite mapping from V to W. We write µ[ X ← d ] for the store σ such that σ(X i ) = d i and σ(Y ) = µ(Y ) for Y = X i , where i = 1, n for some fixed n. We write dom(µ) to mean the domain of µ.

Rules to evaluate expressions are given in Figure 3. Each operator of arity n is interpreted by a total function op : W n → W. The relation µ E ⇒ t d means that the expression E is evaluated within t steps to d ∈ W, where each variable in V(E ) is in dom(µ). We just write µ E ⇒ µ if we don't care about the running time.

Variables µ X ⇒ 1 µ(X ) Op µ E 1 ⇒ t1 d 1 . . . µ E n ⇒ tn d n µ op(E 1 , . . . , E n ) ⇒ 1+ n i=1 ti op (d 1 , . . . , d n ) Fig. 3

. Time semantics of Expressions

Command execution rules are given in Figure 4. Given a store µ, the relation µ C ⇒ t µ expresses that the command C returns the store µ and terminates within t steps. We write µ C ⇒ µ if we don't care about the running time. A command C does not terminate in a given store µ, if there is no µ and no t such that µ C ⇒ t µ . In this case, we write µ C ⇒⊥.

A program P is given by a command C , a list of input variables X 1 , . . . , X n , and an output variable Y . A program computes a partial function P from W n to W defined by

P (d 1 , . . . , d n ) = µ(Y ) iff µ 0 [ X ← d ] C ⇒ µ
where for each variable Z in C , µ 0 (Z ) = ff. A program is terminating iff P is a total function. The program running time is the partial function Time P from W n to N defined by

Time P (d 1 , . . . , d n ) = t iff µ 0 [ X ← d ] C ⇒ t µ
The length of a word d is denoted |d |. A program P is running in polynomial time if there is a polynomial Q such that for all d 1 , . . . , d n , Time P (d 1 , . . . ,

d n ) ≤ Q(max i (|d i |)).

IV. SAFE PROGRAMS A. Neutral and positive operator interpretations

We present a restriction on operator interpretations. For this we shall define two kinds of operator interpretations called neutral and positive. But before, we present some typical operators with their interpretations over W to illustrate definitions.

• For each word v , we have an operator eq v which tests whether or not a word begins with a given prefix v .

eq v (u) = tt if u = v .d for some d ff otherwise

• We have an operator pred , which deletes the first letter of a word such that

pred (u) = if u = u if u = i.
d and for some d and letter i

• For each word v , we have an operator suc v satisfying suc v (u) = v .u. Now, define as the sub-word relation over W by u d , iff there are v and v such that d = v .u.v where . is the concatenation.

An operator op has a neutral interpretation if either 1) either op : W → {tt, ff} is a predicate; or 2) or for all d 1 , . . . , d n , op (d 1 , . . . , d n ) d i for some i ≤ n. The operators eq v and pred have a neutral interpretation.

An operator op has a positive interpretation if there is a constant c op such that

| op (d 1 , . . . , d n )| ≤ max i (|d i |) + c op
The operator suc v has a positive interpretation.

Remark 1: A neutral interpretation is also a positive interpretation. But the converse is false.

Assign Γ(X ) = α Γ, ∆ E : (α, β) α α Γ, ∆ X :=E : (α, β) Compose Γ, ∆ C : (α, β) Γ, ∆ C : (α , β ) Γ, ∆ C ; C : (α ∨ α , β ∨ β ) If Γ, ∆ E : (ρ, ρ ) Γ, ∆ C : (α, β) Γ, ∆ C : (α, β) where α ρ Γ, ∆ if E then C else C : (α, β) While Γ, ∆ E : (α, α ) Γ, ∆ C : (α, β) where β ≺ α Γ, ∆ while(E ){C } : (α, β) Fig. 2. Type system for commands Update µ E ⇒ t d µ X :=E ⇒ t+1 µ[X ← d ] µ C ⇒ t µ µ C ⇒ t µ µ C ; C ⇒ t+t µ Sequence Branch µ E ⇒ t tt µ C ⇒ t µ µ if E then C else C ⇒ t+t +1 µ µ E ⇒ t ff µ C ⇒ t µ µ if E then C else C ⇒ t+t +1 µ While µ E ⇒ t ff µ while(E ){C } ⇒ t µ µ E ⇒ t tt µ C ⇒ t µ µ while(E ){C } ⇒ t µ µ while(E ){C } ⇒ t+t +t +1 µ

B. Positive and neutral operators and safe environment

Assume that ∆ is an operator typing environment. A constant is neutral if all its types the type w.r.t. ∆ satisfy (α, β) where β α. An n + 1-ary operator is neutral if all its types w.r.t. ∆ satisfy

(α 1 , β 1 ) . . . → (α n , β n ) → (∧ i=1,n α i , ∨ i=1,n β i ) where ∨ i=1,n β i ∧ i=1,n α i .
A n-ary operator is positive if all its types w.r.t. ∆ satisfy

(α 1 , β 1 ) → . . . → (α n , β n ) → (∧ i=1,n α i , ∧ i=1,n α i )
Next, if each operator op in the domain of ∆ is neutral or positive then we say that ∆ is a safe typing environment. Throughout this article, we consider safe operator typing environments.

Remark 2: Depending on an operator typing environment ∆, an operator may be neutral and positive at the same time.

Lemma 1 (Tier unicity): Assume that Γ is a variable typing environment and ∆ is a safe operator typing environment. There is a unique tier α such that Γ, ∆ E : (α, β).

Proof: By induction on E . If E is a variable, the conclusion follows immediately. Suppose that E = op(E 1 , . . . , E n ).

Since ∆ is safe, op is either neutral or positive. In either case, α = ∧ i=1,n α i , where the type of each E i is (α i , β i ). By induction hypothesis, α i is unique. So α is also unique by lattice definition.

Remark 3: In contrast to this, β is not unique because it represents the current level of classification of an object, and so this level may vary depending on the context in which an expression is used. Typically, a variable of tier 1 can be an expression of type (1, 0) or (0, 0).

C. Main Result

Assume that ∆ is a safe operator typing environment, and Γ a variable typing environment. A program P defined by a command C is well-typed if Γ, ∆ C : (α, β) where (α, β) is the type of P.

We now define a relation between the operator interpretation and its types given by ∆. A program is safe if (i) it is well-typed, if (ii) each operator has a neutral or a positive interpretation and if (iii) each operator which has a neutral (positive) interpretation is neutral (positive) w.r.t. ∆.

Theorem 1: Let ({0, 1}, , 0) be the complexity lattice. A terminating and safe program is computable in polynomial time. Conversely, every polynomial time function over the set of words W is computable by a terminating and safe program.

Proof: If the type of a safe program over ({0, 1}, , 0) is (0, 0) then the running time is constant because there is no loop. If its type is (1, 0), then we use Lemma 11. Finally, if its type is (1, 1), then we use Lemma 13.

The converse is a consequence of Theorem 2.

D. Examples

We present three examples over the natural numbers. We posit that natural numbers are encoded by words in unary. The complexity lattice is ({0, 1}, , 0). We consider a positive operator +1 in infix notation. Types of the operator +1 w.r.t. ∆ are (0, 0) → (0, 0), (1, 0) → (1, 1), and (1, 1) → (1, 1). We also consider two neutral operators : -1 and a unary predicate > 0, both in infix notation. Types w.r.t. ∆ are (0, 0) → (0, 0), (1, 0) → (1, 0) and (1, 1) → (1, 1). Thus, the typing environment ∆ is safe. So all programs below are safe.

The type of each command is written at the end of the line. We use labels for tiers. For example X 1 means that the tier of X is 1.

1) Addition: Let us now examine the addition.

Add(X 1 , Y 0 ) { w h i l e (X 1 > 0) { X 1 :=X 1 -1 : (1, 0) Y 0 :=Y 0 + 1 : (0, 0) } : (1, 0)
The typing derivation is given in Figure 5. We see that the while-loop is controlled by X , which is of tier 1. The whiletyping rule enforces the body-loop is of type (1, 0). Therefore, all commands inside the body-loop are of type (1, 0) or (0, 0). As a result, the variable Y must be of tier 0 and the operator +1 of type (0, 0) → (0, 0). The assignment X 1 :=X 1 -1 is a typical case of declassification. The variable X of tier 1 is first downgraded to an expression of type (1, 0). Then, we apply a neutral operator, here -1 with the type (1, 0) → (1, 0). We get a declassified expression X -1 of type (1, 0), that is assigned to X by a command of type (1, 0). One can intuitively see that Y can not be of tier β because in this case Y 0 :=Y 0 +1 should be of type (1, 1), which will violate the typing condition on while-loop.

2) Multiplication: Both inputs are of tier 1 and the output Z is of 0.

Mul(X 1 , Y 1 ) { Z 0 :=0 : (0, 0) w h i l e ( X 1 > 0 ) {X 1 :=X 1 -1 : (1, 0) U 1 :=Y 1 : (1, 0) w h i l e ( Y 1 > 0 ) { Y 1 :=Y 1 -1 : (1, 0) Z 0 :=Z 0 + 1 : (0, 0) } : (1, 0) Y 1 :=U 1 : (1, 0) } : (1, 0) } : (1, 0)
The typing derivation of U

1 :=Y 1 is Γ(U ) = 1 Γ(Y ) = 1 Γ, ∆ Y : (1, 0) Γ, ∆ U :=Y : (1, 0)
3) Greatest Common Divisor: The program below computes the greatest common divisor of X and Y . The result is stored in Z . For this, we need subtraction that we define as a neutral operator. Indeed, we have d -u d w.r.t. the unary encoding of natural numbers. We also need the predicate X > Y . We assign to both of them the neutral type (1, 0) → (1, 0) → (1, 0) in the typing derivation of Gcd presented below.

Gcd(X 1 , Y 1 ) { i f ( X 1 > 0 ) t h e n { w h i l e ( Y 1 > 0 ) { i f ( X 1 > Y 1 ) t h e n X 1 :=X 1 -Y 1 : (1, 0) e l s e Y 1 :=Y 1 -X 1 : (1, 0) } : (1, 0) Z 1 :=X 1 : (1, 0) } : (1, 0) e l s e Z 1 :=Y 1 : (1, 0) } : (1, 0)
4) Search: The program below searches for v in a word X . For this, take two constants tt and ff to denote tt and ff of type (1, 0).

Search(X 1 ) { find:=ff ; : (1, 0) loop:=tt ; : (1, 0) w h i l e ( loop ) { i f eq v (X ) t h e n find:=tt ; loop:=ff ; e l s e i f ( X == ) t h e n loop:=ff ; e l s e X :=pred (X ) ; } } : (1, 0)

It is necessary that the tier of X is 1 in order to be able to modify the tier 1 variable loop which guards the whileloop. As a consequence, each command inside the two nested if-then-else is of type (1, 0).

V. CHARACTERIZING POLYNOMIAL TIME FUNCTIONS

We now provide a simulation of polynomial time Turing machines by safe and terminating programs.

Fig. 1 .

 1 Fig. 1. Type system for expressions

Fig. 4 .

 4 Fig. 4. Timed semantics of Commands

Theorem 2 :

 2 Every polynomial time function over the set of words W can be computed by a safe and terminating program.Proof: A unary polynomial time function f on W is computed by a Turing Machine M , with one tape and one head, within (n + 1) k steps for some constant k where n is the input size. The tape of M is represented by two variables Left and Right which contains respectively the left side of the tape and the right side of the tape. States are encoded by fixed sized words and the variable State contains the current state. The tier of the three variables holding a configuration of M is 0. A one step transition is simulated by a finite cascade of if-commands of the form:Γ(X ) = 1 Γ, ∆ X > 0 : (1, 1) Γ(X ) = 1 Γ(X ) = 1 Γ, ∆ X : (1, 0) Γ, ∆ X -1 : (1, 0) Γ, ∆ X :=X -1 : (1, 0) Γ(Y ) = 0 Γ(Y ) = 0 Γ, ∆ Y : (0, 0) Γ, ∆ Y + 1 : (0, 0) Γ, ∆ Y :=Y + 1 : (0, 0)Γ, ∆ {X :=X -1; Y :=Y + 1} : (1, 0) Γ, ∆ while(X > 0){X :=X -1; Y :=Y + 1} :[START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF] 0)

Fig. 5 .

 5 Fig. 5. Typing derivation of add

ACKNOWLEDGMENT

The author would like to thank Gérard Boudol and Daniel Leivant.

The command above expresses that if the current read letter is a and the state is s, then the next state is s , the head moves to the right and the read letter is replaced by b. Since each variable inside the above command is of type (0, 0), the type of the if-command is also (0, 0).

The iteration is made by nested k-while-loops. For this, we use k variables X1, . . . , Xk of type 1.

X1 1 :=X 1 / / t h e i n i t i a l v a l u e w h i l e ( X1 1 > 0 )

{ X1 1 :=X1 1 -1 : (1, 0) X2 1 :=X 1 : (1, 0) w h i l e ( X2 1 > 0 ) { X2 1 :=X2 1 -1 : (1, 0) X3 0 :=X 1 : (1, 0) . . .

The guard of each loop is of tier 1. On the other hand, the body of each loop is of tier (1, 0) because first the step command is of type (0, 0) and second each variable of type (1, 0) is assigned neutral operators or variables of the same type.

VI. TYPE SOUNDNESS FOR EXPRESSIONS

We begin with a lemma, which says that the type system for expressions is sound, with respect to declassification policy.

Lemma 2 (Expression declassification): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. If Γ, ∆ E : (α, β), then β α.

Proof: The proof goes by induction on expressions and uses the fact that operators are either neutral or positive.

The following lemma, called simple security, says that only variables at level α or higher will have their contents read in order to evaluate an expression E of type (α, β). Over the two tier lattice ({0, 1}, , 0), if α = 1, E is evaluated without reading any tier 0 variables. This property corresponds to the rule "no read down" of Biba's model. This reveals also some similarities with Myers' and Liskov's decentralized label model [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF] where each object has an owner and a list of readers which this owner permits to read the data.

Lemma 3 (Simple security): Assume that Γ is a variable typing environment. Assume also that ∆ is a safe operator typing environment. If Γ, ∆ E : (α, β), then for every X ∈ V(E ), we have Γ(X ) α.

Proof: The proof is done by structural induction on E . The base case is when E is a variable. The typing judgement yields Γ(X ) α. Suppose that E = op(E 1 , . . . , E n ). There are two cases to examine since ∆ is safe.

• op is a neutral operator. Then its type is

By induction hypothesis, for each X in E i we have Γ(X ) α i . Again, Γ(X ) ∧ i=1,n α i .

VII. TYPE SOUNDNESS FOR COMMANDS

The two following lemmas state properties on command types which are useful in other proofs.

Lemma 4 (Command declassification): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Assume also Γ, ∆ C : (α, β). Then β α.

Proof: By Lemma 2 and by observing that if β α and β α then β ∨ β α ∨ α . Lemma 5 (Monotonicity): Assume also that C is a subcommand of C and that Γ, ∆ C : (α, β) where ∆ is safe. Then, Γ, ∆ C : (α , β ), where α α and β β. Proof: By induction on typing derivation length. The following lemma corresponds to the write access rule of Biba's model, which states that a command can write data of lower level than itself. In our context, if a command C has the type (α, β) then Confinement lemma says no variable of rank above tier α is updated in C . Lemma 6 (Confinement): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Assume also Γ, ∆ C : (α, β). Then, for each variable X assigned to in C , Γ(X ) α.

Proof: By induction on C . Suppose that Γ, ∆ X :=E : (α, β) by (Assign). There is α such that Γ(X ) = α α. The other cases follow directly by induction.

We are now ready to establish type soundness theorem, which states a first non-interference property. Over ({0, 1}, , 0), type soundness theorem states that if X is variable of tier 1, then we can arbitrarily alter the value of a variable Y of tier 0, execute again the command C , and the value of X will be the same. As we shall see in a short while, this noninterference property has a strong consequence on the loop length.

Theorem 3 (type soundness): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Assume also that 1)

for each variable X such that Γ(X ) τ . Then for every variable X such that Γ(X ) τ , we have µ (X ) = σ (X ).

Proof: By induction on the structure of the derivation µ C ⇒ µ .

Suppose that the last rule of the evaluation under µ is

and that the evaluation under σ ends with σ

The typing ends with an application of rule (Assign)

There are two cases to consider:

τ by transitivity. From hypothesis 5, we have

, for all variables Y such that Γ(Y ) τ by Hypothesis [START_REF] Leivant | A foundational delineation of poly-time[END_REF]. Suppose that µ while(E ){C } ⇒ t µ and that σ while(E ){C } ⇒ t σ and the typing ends with

There are again two cases to consider.

• α τ . By simple security Lemma 3, for each variable

The conclusion is immediate in the case d = ff. On the other case, d = tt, the evaluation under µ ends with

and the evaluation under σ ends with

τ . So we can again apply the induction hypothesis. We have µ (X ) = σ (X ) for all X such that Γ(X ) τ .

• α τ . For every X assigned to in C , we have Γ(X ) α by confinement Lemma 6. Since is transitive, Γ(X ) τ . Therefore, no variable of type τ is updated during the execution of this loop. The other cases are similar.

VIII. UPPER BOUNDS ON LOOP LENGTH

We now move on the issue of bounding the length of while loops for terminating commands. Given a variable typing environment Γ and a safe operator typing environment ∆, a loop while(E ){C } is of tier τ if Γ, ∆ E : (τ, τ ). Note that Lemma 1 implies that loop tiers are unique. Note also that the tier of each loop in C is less or equal than τ , because of Lemma 5.

We define a loop length semantics in Figure 6, which measures the length of loops of tier τ forgetting, intuitively, all loops of different tiers. The derivation µ Γ,∆ C → t τ µ means that the run of C under µ performs t iterations of tier τ . This loop length semantics is correct in two ways. First it is sound w.r.t. big step semantics, that is if µ C ⇒ t µ then µ Γ,∆ C → tτ τ µ and t τ ≤ t for any tier τ . Second, it is correct with respect to time usage, which is established by Theorem 4 below.

Lemma 7:

Because the cost of an operator is 1. Theorem 4: Let (SC, , 0) be a complexity lattice. Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Given a command C , there is a constant

Temporal non-interference is a consequence of noninterference Theorem 3, which claims that values of tier 1 variables don't depend on values of lower tier variables. Temporal non-interference theorem says the length loop of tier τ depends only on variables of tier τ . Over the two tier lattice ({0, 1}, , 0), all loops are of tier 1. So, Temporal

Update

Fig. 6. Loop length semantics of tier τ non-interference means that the length of the loop depends on tier 1 variable. A modification in the value of a variable of tier 0 does not affect loop lengths. Note that temporal noninterference is related to Lemma 4.1 of [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF], which states that the computation length is bounded by a polynomial in the size of normal inputs.

Theorem 5 (Temporal non-interference): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Assume also that 1)

Proof: By induction on the structure of the derivation µ Γ,∆ C → t τ µ . Suppose that µ Γ,∆ while(E ){C } → t τ µ and that σ Γ,∆ while(E ){C } → t τ σ and the typing ends with

There are three cases to consider.

• α τ . By simple security Lemma 3, for each variable

In the case d = ff, we have t = t = 0. On the other case, d = tt, the evaluation under µ ends with

and the evaluation under σ ends with

σ Soundness Theorem 3 implies that for every variable X such that Γ(X ) τ , µ (X ) = σ (X ). So by induction hypothesis, t 1 = t 1 and t 2 = t 2 . Therefore t = 1 + t 1 + t 2 = 1 + t 1 + t 2 = t . • α τ . There is no loop of tier τ in C . So t = t = 0. Other cases are consequences of Soundness Theorem 3

Temporal non-interference provides a weak termination criterion. Take again the two tier lattice ({0, 1}, , 0). Theorem 5 says the length of a loop depends only on configurations of tier 1 variables. So, if we enter twice into a loop with the same configuration of variables of tier 1, we are sure that the loop will never terminate. Indeed, this configuration of tier 1 variables will never change. This argument is formalized in the next corollary.

Corollary 1: Assume that Γ, ∆ E : (α, α ) and Γ, ∆ C : (α, β) where ∆ is a safe operator typing environment. Assume that (µ i ) i is sequence satisying µ i C ⇒ µ i+1 such that there is k > 0 satisfying both conditions:

1) for each i < k, µ i E ⇒ tt.

2) for all X ∈ V(C ), Γ(X ) β, µ 0 (X ) = µ k (X ). Then, µ 0 while(E ){C } ⇒⊥. In other words, while(E ){C } does not terminate from µ 0 .

Proof: Suppose for the sake of contradiction that there is T such that µ 0 while(E ){C } ⇒ T µ. There are t and t such that µ 0 while(E ){C } → t α µ and µ k while(E ){C } → t α µ. Since α β, Theorem 5 implies that t = t . On the other hand, we have t < t since k > 0. This leads to a contradiction. So, while(E ){C } does not terminate from µ 0 .

IX. NEUTRAL TERMS

A neutral term is an expression which is just built up from variables and neutral operators.

Lemma 8: Assume that Γ is a variable typing environment. Assume also that ∆ is a safe operator typing environment. If Γ, ∆ E : (α, β), where β ≺ α then E is a neutral term.

Proof: We show by induction on E that if E contains a positive operator, then α = β. As a result, the lemma will be proved. Suppose that E = op(E 1 , . . . , E n ). It is immediate if op is a positive operator. Otherwise, op is a neutral operator of type (α 1 , β 1 ) → . . . → (∧ i=1,n α i , ∨ i=1,n β i ), where ∨ i=1,n β i ∧ i=1,n α i and which contains a sub-expression E i with a positive operator. By induction hypothesis, we have

Lemma 9 (Neutrality): Assume that Γ is a variable typing environment and that ∆ is a safe operator typing environment. Assume also Γ, ∆ C : (α, β), where β ≺ α. Let X be a variable such that Γ(X ) β. Then, if X is assigned to in C , then it is always assigned to a neutral term.

Proof: Take an assignment of C where Γ(X ) β and consider its typing rule:

The last step is to determine an upper bound on the number of possible values of variables of tier strictly greater than β, which are computable by iterating a command C of type (α, β). Then it follows from Corollary 1 that this upper bound is also an upper bound on the length of while(E ){C }.

For this, we consider a command C and a store µ. We define the set R k µ (C ) of reachable stores from C and µ in k steps by

as the set of reachable stores from C and µ.

Let Γ be a variable typing environment such that dom(Γ) = dom(µ). Define µ ↑β as the restriction of µ to variables of tier strictly greater than β:

Lemma 10: Let ∆ be a safe operator typing environment. Assume that P is a safe program given by a command C and that Γ, ∆ C : (α, β) where β ≺ α. Then, there is a polynomial Q such that for all stores µ, #R C (µ) ↑β ≤ Q(n)where n = max Γ(X ) β (|µ(X )|). (#S is the cardinal of the set S.)

Proof: Let X be a variable assigned to in C such that Γ(X ) β. Lemma 9 states that X is assigned to a neutral term E . From this observation and because of the interpretation of neutral operators, we show by induction on k that for each µ in R k µ (C ) and each variable X , Γ(X ) β, µ (X ) is either in the range of some finite neutral interpretation (i.e. predicates), or there is Y such that µ (X ) µ(Y ) and Γ(Y )

β by lemma 3.

Since the number of sub-words of a word of size n is bounded by n 2 , #R C (µ) ↑β is bounded by Q(n) which only depends on C .

Thus, the length of a while-loop while(E ){C } is bounded by the number of stores in R C (µ) ↑β where the type of C is (α, β).

X. COMPLEXITY BOUNDS

Assume that P is a safe program given by a command C . We establish upper bounds on program runtime with respect to the program type.

Lemma 11: Let ∆ be a safe operator typing environment. Assume that Γ, ∆ C : (α, 0). There is a polynomial T such that for all stores µ, if µ C ⇒ t µ then t ≤ T (n) where n = max Γ(X ) 0 (|µ(X )|).

Proof: All while loops in C are of tier 0. By Theorem 5, the length of loops depends only on variables of tier 0. By setting β = 0 in Lemma 10 , we see that the number of reachable values of tier 0 is bounded by Q(n), where Q is a polynomial. And Corollary 1 states that length of loops is bounded by the number of reachable values of tier 0. Therefore, the length of loops is bounded by Q(n). By Theorem 4, the runtime is bounded by

Lemma 12: Let ∆ be a safe operator typing environment. Assume that Γ, ∆ C : (α, α). There is a constant c such that for all stores µ, if µ C ⇒ t µ then for every X such that Γ(X ) = α, we have |µ

Proof: Take an assignment X :=E occurring in C , where Γ(X ) = α. There are two cases. First, the type of E is (α, α). So, X :=E is not inside a loop body. Otherwise, the typing rule (While) would be violated. Second, the type of E is (α, β), where β ≺ α by Lemma 2. By Lemma 8, E is a neutral term. So, simple security Lemma 3 implies that, in both cases, we have |µ (X )| ≤ max Γ(Y ) α (|µ(Y )|) + c for some constant c.

Lemma 13: Assume that the complexity lattice is ({0, 1}, , 0). Let ∆ be a safe operator typing environment. Assume that Γ, ∆ C : (1, 1). There is a polynomial T such that for all stores µ, if µ C ⇒ t µ then t ≤ T (n) where n = max Γ(X )=1 (|µ(X )|).

Proof: By combining Lemmas 11 and 12.

XI. A CRITERION OF WEAK TERMINATION

In our situation, non-interference property provides a termination criterion in the following sense:

Theorem 6: Let ∆ be a safe operator typing environment. Assume that Γ, ∆ C : (α, 0). There is a polynomial decision procedure which given a store µ decides whether or not there is µ such that µ C ⇒ µ .

Proof: Corollary 1 implies that it suffices to check if there are two stores whose values assigned to variables of tier 0 are identical. The runtime of the decision procedure is polynomial time computable because Lemma 10 implies that it suffices to memorize a polynomial number of stores.

XII. CONCLUSION

We think that concepts underlying type systems for secure information flow analysis provide new directions to characterize program complexity. There are several issues to investigate like the ones that are listed below.

A major question is intensionality and language expressiveness, which is crucial in order to apply methods related from ICC. Security typed languages are now expressive and we could maybe take advantage of works already made in order to analyze resource usage of a broader class of sequential or parallel algorithms. A first step would be to enlarge the class of neutral terms by, for example, re-using des-allocated spaces, like this has been done by Hofmann [START_REF] Hofmann | Linear types and non-size-increasing polynomial time computation[END_REF].

The role of complexity lattice was reduced in this paper because our study is on polynomial time computation, which is a robust sequential class. On the other hand, complexity lattice may be an interesting tool to study small complexity classes and to to study the complexity of process calculus computation with respect to causality see e.g. [START_REF] Demangeon | Static and dynamic typing for the termination of mobile processes[END_REF].

We restrict the domain of values to a set of words. Results may be extended easily for several data-structure like array of words, lists, . . . However to go further, it should be interesting to follow Dal Lago & Martini [START_REF] Lago | An invariant cost model for the lambda calculus[END_REF] and to deal with more complex data structures. Another direction is also to study the introduction of weak operators like parity which declassify (or classify) a small amount of information.

A practical approach may combine other approaches that we have already mentioned in the discussion on related works. In particular, a static analysis based on our approach could be made by compiling a source program into an abstract program with respect to resource consumption. Here, we follow ideas suggested [START_REF] Ben-Amram | Linear, polynomial or exponential? complexity inference in polynomial time[END_REF] and [START_REF] Jost | Static determination of quantitative resource usage for higher-order programs[END_REF]. Then, the complexity of a source program could be obtained from a type inference algorithms.

Conversely, we may wonder if methods developed in ICC, and in particular light linear logic approaches, can be used and bring something new to security-type systems.