François Toutain
email: francois.toutain@orange.com

Ahmed Bouabdallah
email: ahmed.bouabdallah@telecom-bretagne.eu

Radim Zemek
email: radim.zemek@orange.com

Claude Daloz
email: claude.daloz@orange.com

Methodological Introduction of Context Awareness in the Design of 3GPP Conversational Services

Keywords: Context Awareness, Multimedia Telephony, Supplementary Service, Methodology, Taxonomy. I

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Methodological Introduction of Context Awareness in the Design of 3GPP Conversational Services

François Toutain INTRODUCTION Supplementary services such as Call Forwarding on No Reply (CFNR), Call Waiting (CW), or Closed User Group (CUG) complement basic call services [1] and are commonly used in professional settings while their usage is somewhat less developed in mass market situations. Totalling nowadays more than twenty different functions, supplementary services have a long history, coming from legacy ISDN (Integrated Services Digital Networks) [START_REF]ISDN User Part Supplementary Services[END_REF]. ETSI (European Telecommunications Standards Institute) quickly introduced them in GSM [START_REF][END_REF] and in the same vein 3GPP (Third Generation Partnership Project) adopted them for the UMTS architectures without major evolution until Release 6. Adaptation of these features to IMS (IP Multimedia Subsystem) and NGN (Next Generation Network) was first pioneered by ETSI TISPAN (Telecom and Internet Converged Services and Protocols for Advanced Networks) [START_REF]Multimedia Telephony with PSTN/ISDN simulation services -V1.1[END_REF]. 3GPP taken up part of ETSI works began in Release 7 the development of MMTel (Multimedia Telephony service) [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF]. 3GPP has afterwards been entrusted the mission to continue the unified and coherent development of MMTel together with common IMS. Last but not least supplementary services held also attention of GSMA (GSM Association) which introduces part of them in its work concerning the definition of an IMS Profile for Voice and SMS [START_REF] Prd Ir | IMS Profile for Voice and SMS[END_REF].

It is no surprise that these services have been specified through a large standardization body. Indeed, standardization processes are of critical importance for interoperability issues and consistent behaviour leading to wide adoption. That's why basic telecommunication services benefited of such a huge standardization effort. But, although they are very widely known, supplementary services are not really massively adopted as it has been the case for example about SMS (Short Message Service) or mobility, except for the professional area where the specific needs of large and small businesses have led to a marginally wider use. The reasons of such a situation may be quite complex; it appears however that the poor quality of experience emerging from the usage of these supplementary services, constitutes one of its main explanatory factor. Let's first remark that past implementations of these features as well as current ones offer very mediocre dial-based interfaces, which make them difficult and awkward to use [START_REF] Norman | The Design of Everyday Thing[END_REF]. They exhibit very limited and rigid behaviour. And due finally to the "walled-garden networks" principle governing network operators' policies, these features are devoid of any customization capability. Last but not least, the feature interaction problem, which is a quite complicated matter far from being completely solved, often precludes the simultaneous use of these various service elements [START_REF] Turner | Goals and Conflicts in Telephony[END_REF].

With all these drawbacks, it is no surprise that network operators around the world have hardly promoted the majority of supplementary services, and have fallen back on simple strategies such as default provisioning within packaged subscription plans. However, we believe that the attention toward supplementary services may soon increase significantly. Indeed, there is a current interest boasted by the introduction of next generation networks, such as 4G/IMS (IP Multimedia Subsystem), through the MMTEL specification efforts [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF]. We can also quote as a recent trend the RCS initiative (Rich Communication Suite) which aimed at large audiences, and was however reduced later on to the RCS-e [START_REF][END_REF] (basically because of cost structures and thus a requirement to reduce the introduction cost of these new technologies). In addition, the mass market penetration of smartphones is reaching unprecedented levels, and these powerful terminals, equipped with large screens are beginning to offer renewed basic services, taking advantage of the smartphone capabilities, such as the visual voicemail feature (provided eg. on Apple's iPhone or Android-based mobile terminals).

Our thesis in this paper is that these increased capabilities, available on smartphone-class terminals for an increasing number of subscribers, are an opportunity to provide supplementary services which will be easier to configure and use. Indeed, these capabilities are key to offer a better user experience, and so far, this has been almost exclusively the case for over-the-top services, implemented by third parties having nothing in common with network operators, while the classical communication services have been kept to a very basic level of functionality. This evolution has leaded to the current situation, where there is a clear dichotomy between advanced services which benefit from capabilities of new platforms but are not standardized, leading to fragmentation, and classical services, standardized but lacking from improved user experience.

In an attempt to improve the situation without restricting the market to high end terminals, the RCS initiative considered ambitious features such as an enhanced phonebook, enriched communications with content sharing capabilities, and enhanced messaging services. It was however reduced to RCSe which focuses on capability sharing, and basically ignored classical supplementary services [START_REF][END_REF]. MMTEL which could appear as the standard side of RCS, relies on the NGN 's generalized conversational session between mobile or/and fixed users involving various media (speech, video, text, …); like RCS-e MMTEL introduces sharing capabilities but differently from it, authorizes an enrichment of a session through the execution of updated versions of supplementary services [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF][10] deployed in dedicated SIP application server called TAS (Telephony Application Server) [11].

One interesting approach close to RCS/MMTEL initiatives is that of context awareness. Indeed, context could be one of the ways to make services flexible and adaptive. Context aware systems are defined as ones which can adapt their behaviour depending on changing user situations (context adaptation), and also as systems able to explicitly present context data to the users (context presentation) [START_REF] Toutain | Interpersonal contextaware communication services[END_REF]. Context-awareness has been studied for many years, with strong results, and already some independent services being deployed (e.g. GrandCentral aka Google Voice, OneNumber). We believe that now is the proper time to bring context to core services, because, although these are well-known services, context awareness could well enhance the subscribers' willingness to use them. We also advocate that it is an important matter to push this approach to standardization.

In this paper we analyze existing supplementary services, and we introduce a methodology allowing us to produce context-aware versions of those services. Usage of such context-aware services is illustrated by some use cases. A global taxonomy of conversational services applied to supplementary services concludes the paper together with the analysis of the methodology and the pending issues.

II. PRESENTATION OF THE METHODOLOGY

Before exposing our methodology for adding contextawareness to communication services, we must introduce some technical definitions. In this paper, context is defined as soft real-time information pieces related to a user situation, be it some physical measurement, logical status, or a combination of several such data [START_REF] Toutain | Interpersonal contextaware communication services[END_REF]. Context is usually acquired through some low-level systems, e.g. sensors, and/or derived from logical information. Low-level context data may further be processed into higher level information, using a variety of techniques such as logical inference or data fusion. Examples of context data include weather condition, localization, user's availability, current agenda slot, number of people around user, etc.

Our focus in this paper is to define context-aware conversational/interpersonal services, starting from classically defined call services in 3GPP or equivalently communication services in the MMTEL standardization effort. These services obey a well-defined life-cycle, by which [13] :

• a user subscribes to service S ;

• upon approval, the service operator provisions S, using some predefined data coming in part from the user and in part from the operator itself (these parameters being operator embedded data, freely chosen within the standards constraints in order to match a specified service level) ;

• depending on the service, activation can be performed by the operator after which they are always-on services, or activation can be done bit by bit by the user herself ;

• invocation can be implicit (for always-on services), or explicit by the user. In the latter case she can provide some parameters during invocation ;

• deactivation can be performed for some services ;

• widthdrawal of the service is the last step.

These services specifically target operator networks, meaning that all the operations occurring in the network are strictly and closely controlled by the operator [START_REF] Bouabdallah | On the Benefits of a Network-Centric Implementation for Context-Aware Telecom Services[END_REF].

Studying the addition of context-awareness to these services can be done in a systematic manner. This is the purpose of the following methodology. Trend 1 is concerned with the service parameters. Conversational services somehow control the calls placed by users, using specific informations provided by the network operator or by the user herself. Static parameters are defined during the service subscription, usually by selecting proper designed values, fixed by the operator at service creation time, are more rarely by the user. Dynamic parameters are input by the user at service invocation time. Context situations can obviously have an influence on these parameters. Previously static parameters can become more dynamic, thanks to changing context data ; and dynamic parameters can come from context situations, instead of being input by the user, or in addition to it. An example of static parameter becoming context-aware is the no answer timer in the CFNR feature [START_REF]Communication Diversion (CDIV) using IP Multimedia (IM) Core Network (CN) subsystem[END_REF]. In current services instances, operators have to decide on a fixed, good-for-all value for the timer, before the service forwards the incoming call to its new target (e.g. the voicemail system). In a context-aware CFNR feature, the timer can be adapted, for instance, after a learning phase allowing to finetune it to every single user. An example for a dynamic parameter could be the target number of the same service, which could make use of the pro/perso status of the user to change the targeted number, and send private calls to private voicemails whereas professional calls would be routed to a colleague's office.

Trend 2 deals with the service triggering, by which is meant service invocation on the user side, or service activation on the operator's part. In classical implementations, these operations are performed in a static way, so that a service is always-on, or is available on user's request. Using context-awareness, we can change this behaviour, so that a service can be triggered depending on some context condition, which can be very dynamic in nature. As an example, consider the Call Deflection (CD) feature, by which a user terminal is able to avoid the user being interrupted by an incoming call, by deflecting it to another destination [START_REF]Communication Diversion (CDIV) using IP Multimedia (IM) Core Network (CN) subsystem[END_REF]. In a classical implementation, the user must activate the CD service and provide a target identification for the potential bouncing calls. In a context-aware version of this service, users' activity, e.g. driving a car, can be automatically used to infer that users are busy, and the service can be autonomously activated. Conversely, the service triggering can also be inhibited due to context conditions. An example is an emergency call that could get through the CD service.

Trend 3 is about unifying several services when they can relate to one another thanks to adding some shared context awareness. Indeed, several classical services are very similar except for a specific condition which is explicit in the standards. By relaxing these static condition definitions into a more general context condition, we can unify the services into one, more general, context-aware service. It is interesting to point that 3GPP began to apply this same trend when defining in MMTEL a family of features named Communication Diversion (CDIV) [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF][15] bringing the various forwarding features (Unconditional (CFU), on Busy (CFB), on No Reply (CFNR), on Subscriber Not Reachable (CFNRc), on Not Logged-in (CFNL)) together with the Deflection one (CD). It is however worth noting that even if this regrouping is intuitively well-founded, solid arguments firmly founding it, are still missing. We argue in fact that context awareness can provide the right angle to formally define such unification. We will expand this point more thoroughly in the next section.

Trend 4, finally, relates to relaxing even more the original specifications, and allowing ourselves to "re-think" the services with context-awareness in mind. One example of this trend could be an enhanced Multi Level Precedence and Premption service (eMLPP), which is traditionally specified as an alwayson service allowing to preserve a priori defined, important calls, in times of resource scarcity or network congestion [START_REF]-enhanced Multi-Level Precedence and Pre-emption service (eMLPP) -V10[END_REF]. By relaxing this assumption, we can imagine a dynamic service which, by acquiring a context information pertaining to the subject of the call, by way of word recognition for instance, would be able to classify the call importance dynamically, thus preserving truly important calls instead of predefined ones. Obviously such a service would raise some privacy concerns, as is often the case with context-aware systems [START_REF] Jiang | Modeling Privacy Control in Context-aware Systems[END_REF].

III. METHODOLOGY AT WORK

The main point of trend 1 concerns the contextual derivation of static and/or dynamic parameters used during the invocation of the feature. Lets take CFNR and suppose it has been activated (this is usually the default case in mobile networks [START_REF]Communication Diversion (CDIV) using IP Multimedia (IM) Core Network (CN) subsystem[END_REF]). Its main characteristics concerns the ringing duration controlled by a timer, the value of which, instead of being statically fixed by the operator, could be dynamically decreased/increased according to the context situation. We illustrate this point through various use cases associated to specific contextual situations :

• the context allows us to know that the terminal is not in a reasonable proximity to the callee to let the latter answer the call; a predefined ringing will be useless and we can therefore reduce the timer value to its minimum value (to preserve the integrity of the call log, it is necessary that the callee terminal rings at least once). Proximity between the callee and her terminal can be inferred from various sources which must be combined : accelerometer data from the mobile phone sensor can indicate if the user is currently carrying it ; location of the terminal associated with user agenda could reveal that they don't share the same place, … .

• the context allows us to know that due to her activity, the user is unable to answer the call, because for instance she is currently driving. In this case, the velocity of the terminal can be obtained from the GPS sensor, allowing to deduce that the user is currently moving at a certain speed. This information is not sufficient and must be combined with additional sources, coming in our example from the car system, which may identify the current driver [START_REF] Erdogan | Experiments on Decision Fusion for Driver Recognition[END_REF], and consolidated e.g. with map matching, in order to compare the user trajectory with known roads.

• the context allows us to know that the caller is in distress [START_REF] Yu | Approaches and principles of fall detection for elderly and patient[END_REF], and that her call is implicitly an urgent call. It therefore makes sense, in this case, to extend the ringing duration by increasing the value of the associated timer. A prolonged ringing will be a clear indication to the callee that the call is a special one.

The previous examples manage context information associated to the caller or to the callee. It is interesting to note that when combining both, we may have a service interaction which could be easily solved through priority. Suppose that a caller in distress makes a call to a buddy currently driving. It is reasonable to require that in such a case the no-answer timer duration must be increased (priority to caller situation), to allow the callee to park her car and answer the call.

Trend 2 concerns the dynamical activation of a feature due to specific contextual situation. Suppose the user does not want to be disturbed by a phone call because she is for example at the theater and the context allows us to know this information. It is quite natural when receiving the call, to activate a call deflection feature which will transfer the incoming call to a new address. In our use case, an indoor location system could be used to deduce in an accurate way the right location of the callee; but this information is insufficient and must be combined at least with the exact schedule of the program, to make sure the user cannot currently answer to the call. We note that the value of the new address where to route the deflected call, is a parameter which could also be deduced from the context as explained in trend 1.

Trend 3 may be well illustrated with the forwarding features family defined in the standards. It identifies simple situations of the callee preventing her to answer the call : she is currently already engaged in a call (CFB), or does not answer (CFNR), the call cannot be completed due to internal core network routing problems (CFNRc), the callee is not reachable from the radio access network (CFNRc) or the callee has not registered her terminal (CFNL). All these cases clearly are contextual situations of the callee which can be easily managed thanks to the signalling protocol used to establish the call. If we extend to context not deducible from the signalling protocol but from the state of the callee or of the caller, we are led to define contextual call forwarding as the feature with the capability of modifying, in the core network, the management of the call setup, depending on the caller and callee contexts.

Finally, trend 4 in our methodology deals with reinventing the service, or relaxing assumptions and restrictions imposed by the classical service specification. Applying this view to call forwarding services, we notice that the classical descriptions provide for an optional notification service, by way of which the caller can be notified that her call is being rerouted to a new destination [START_REF]Communication Diversion (CDIV) using IP Multimedia (IM) Core Network (CN) subsystem[END_REF]. This is a clear opportunity to extend the service family, to include a more useful notification, carrying additional information of a contextual nature. For instance, the notification can provide the caller with a reason for the deflection, along with the target of the redirection, e.g. "Alice is currently driving, you are redirected to her voicemail". The same idea applies to situations where the timer parameter is changed: by providing the caller with a better understanding of the callee's situation, one enhances the chances that both parties end up being in contact. For instance, a call which was classified as an emergency one could lead to the caller receiving a notification similar to "Your correspondent is being informed that your call is urgent, please hold on".

IV. ANALYSIS AND ISSUES

The methodology introduced above, can be applied to any general conversational service. We however target in this paper the well-known supplementary services which as indicated in the introduction, have a long history crossing the main areas of telecommunications from ISDN via ETSI GSM, ETSI TISPAN to finally end at 3GPP and GSMA. We may in fact consider two main versions of these features depending on whether they are grafted on a CS-based or IP-based telephony service. These two versions are generally close, but they don't necessarily superpose and they furthermore present occasionally tricky semantic differences justifying their distinction [10]. For the sake of clarity, we will in what follows use the term "feature" or "supplementary service" when the underlying bearer doesn't import, and in the other cases :

• "CS-SS" to identify the ones determined by the direct descendants of the initial ISDN supplementary services [1]

• "IMS-SS" to name the ones arising from the adaptation of supplementary services to IMS and NGN [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF] [START_REF]Multimedia Telephony with PSTN/ISDN simulation services -V2.2[END_REF] Our methodology helped us to develop a comprehensive and systematic introduction of context awareness in all these features. The complete work will deserve by its own a dedicated publication. We identified however during this work a global and structured taxonomy of these features which could be of interest.

A conversational service has the following fundamental characteristics :

• it is structured in three main temporally sequential steps : the establishment, the execution and the release

• it involves at least two principals one of which is the initiator; we name participants the other ones We can organize the existing features in three main functions :

• Presentation concerns the various ways informations can be exchanged (input/output) between a principal and the conversational service through her device

• Authorization identifies various conditions to be met in order to allow or interrupt a particular step of the service together with the verifying process of these conditions and its reporting

• Leg handling determines the different ways to influence the exchange of signaling information between the service and a principal during the three steps We can identify the main characteristics of the existing features as indicated in the table below. Usually supplementary services are often expressed with standardized acronyms. Due to lack of place, we cannot provide the associated glossary; when necessary we advise the reader to consult respectively the two following references : CS-SS [1] and IMS-SS [START_REF]Multimedia Telephony Service and supplementary services -V[END_REF]. It is now clear, based on the variety of service ideas and use-cases exemplified in the previous section, that adding context awareness to communication services can vastly improve their usefulness as well as their ease of use. Nonetheless, several issues are raised by this new approach, including privacy issues, architectural choices, implementation within an operator network of context data processing facilities, or standardization issues.

Privacy is a very real concern to take into account when dealing with context aware services and applications. Besides somewhat idealistic voices which denounce the "big brother syndrome", there is indeed a growing awareness among users that their private life is more and more made transparent to private corporations, with no clear rules to ensure basic rights are respected. As a consequence, for any context aware service to become widely used, its provider has to make considerable effort to ensure and demonstrate its benefits on the one hand, and its rules of play with respect to private data on the other hand. It is understood that some context data are more sensitive to privacy concerns, and that some application classes are better perceived than others. Besides, telecom operators, having a long standing commercial relationships with their subscribers, may be in a good position to act as a trusted party with respect to context data, and they must focus on how to nurture this relationship and how to increase this trust. It is generally accepted that these goals are best reached by providing valuable services in return, and by allowing users to explicitly control their data within the services. Control includes granting access, controlling the level of accuracy, sharing patterns and withdrawal policies [START_REF] Toutain | Interpersonal contextaware communication services[END_REF].

An important aspect of deploying context aware services is related to architecture of the context management system. Many research efforts have been made in this area [START_REF] Toutain | Interpersonal contextaware communication services[END_REF], and we envision that a hybrid approach is a viable one [START_REF] Bouabdallah | On the Benefits of a Network-Centric Implementation for Context-Aware Telecom Services[END_REF], i.e. one where some components are embedded within the core operator network while others can be deployed at the edges, even within the mobile terminals. Some well-known service enablers have already received extensive scrutiny, and they are now widely deployed components, e.g. location management, availability & presence enablers. There is now a requirement to generalize the management of situational data in a carefully designed way. This is specially the case for next generation mobile networks (4G / LTE) where the low latency combined with the high throughputs offered make it eventually possible to gather real-time, multi-dimensional, contextual data about almost any user registered within the network. We are convinced now is the proper time to design a comprehensive context management scheme dedicated to such a mobile network, which is a very important issue for the relevant standardization bodies.

The origin and nature of the context data is also a matter for careful thinking and implementation choices. Actually, two broad categories of contextual data may be thought of: one is "raw data" coming from physical sensors or low-level monitoring services, and the other is "high-level data" resulting from advanced computation such as automated learning, inference or multiple sources consolidation [START_REF] Erdogan | Experiments on Decision Fusion for Driver Recognition[END_REF]. Depending on the service, data from one category or the other may be required, and this has a strong impact on the feasibility of the related service, since sophisticated data may not be easily available for any user at any time (due to processing costs, required infrastructure, but also in some times because of the time it may take to gradually construct the data, as is the case for automated learning or collaborative filtering techniques).

V. CONCLUSION

In this paper, we have proposed to revisit classical telecommunication services by exploring the context awareness dimension. Doing so, we have shown a great potential for renewed services, which become more efficient, more personalized, probably easier to use and more consistent. However, actually implementing these services is a matter for further thinking, because some implementation choices such as service architecture or GUI are of paramount importance for the actual rendering and deserve a lot of attention. The user interface for instance is a critical point for the acceptability of the services, and recent advances such as voice interaction (e.g. Apple's SIRI) may well be key to more natural modes of operation, taking into account that the contextual dimension may well add complexity to the service command.

A similar axis for further work is to adopt the point of view of the operator when designing context-aware services. In the previous sections, we have developed a restrictive view, completely focused on the improvement of the quality of experience of the user, without taking into account the impact of our approach: the resource occupation ratio which has consequences on the financial aspects of the services. But a different study needs to be done which must clearly show the benefits and the cost of introducing context in the business model of such services.

On another level, we argue that the whole lifecycle of the services can be the object of context-aware redesign, and that network management processes, from the point of view of the operator, should be revisited using context.

Extrapolating on our approach, we suggest that the methodology exposed in this paper is general enough to be implemented when designing new context-aware services. A possible approach could be to iterate on a novel service specification, by taking into account trends one to four, in turns, as a way to aid injecting context awareness within the service specification.

Finally, having based our work on standards from the 3GPP consortium, we are considering contributing back to the standardization process, by advocating to turn to context awareness as a major exploration opportunity, for the next evolution steps of the telecommunication services.

Figure 1 .

 1 Figure 1. The building blocks of the methodology Figure 1 depicts four different trends allowing to take context data into account within a service. Trends 1 & 2 are about using context awareness to modify the service mechanisms (implying low-level changes to the services in a systematic approach). Trends 3 & 4 are about revisiting the services in a more creative way (abstracting the service, or reinventing the service by relaxing some prior assumptions in the initial specification).

TABLE I :

 I TAXONOMY OF CS-SS AND IMS-SS

	Establishment	Execution			Release
	CS-SS	IMS-SS	CS-SS	IMS-SS	CS-SS	IMS-SS
	Initiator Participant Initiator Participant Initiator Participant Initiator	Participant Initiator Part.	Initiator Part.


Mariem Graa
email: mariem.graa@it-sudparis.eu

Nora Cuppens-Boulahia

Frédéric Cuppens
email: nora.cuppens@telecom-bretagne.eu

Ana Cavalli
email: ana.cavalli@it-sudparis.eu

Formal Characterization of Illegal Control Flow in Android System

Keywords: dynamic taint analysis, android system, control flows, under-tainting, formal rules, complete algorithm

The dynamic taint analysis mechanism is used to protect sensitive data in the Android system. But this technique does not detect control flows which can cause an under-tainting problem. This means that some values should be marked as tainted, but are not. The under-tainting problem can be the cause of a failure to detect a leak of sensitive information. To solve this problem, we use a set of formally defined rules that describes the taint propagation. We prove the completeness of these rules. Also, we provide a correct and complete algorithm based on these rules to solve the under-tainting problem.

I. INTRODUCTION

Recent years have witnessed an increase in the use of embedded systems such as smartphones. According to a recent Gartner report [START_REF] Uk Egham | Gartner says worldwide mobile phone sales grew 35 percent[END_REF], 417 million of worldwide mobile phones were sold in the third quarter of 2010, which corresponds to 35 percent increase from the third quarter of 2009. To make mobile phones more fun and useful, users usually download third-party applications. For example, we can show an increase in third-party apps of Android Market from about 15,000 third-party apps in November 2009 to about 150,000 in November 2010. These applications are used to capture, store, manipulate, and access to data of a sensitive nature in mobile phone. An attacker can launch flow control attacks to compromise confidentiality and integrity of the Android system and can leak private information without user authorization. In the study presented in Black Hat conference, Daswani [START_REF] Wilson | Many android apps leaking private information[END_REF] analyzed the live behavior of 10,000 Android applications and show that more than 800 were found to be leaking personal data to an unauthorized server. Therefore, there is a need to provide adequate security mechanisms to control the manipulation of private data by third-party apps. The dynamic taint analysis mechanism is used to protect sensitive data in the Android system against attacks [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF]. But this technique does not detect control flows which can cause an under-tainting problem i.e. that some values should be marked as tainted, but are not. Let us consider the attack shown in Figure 1 that presents an undertainting problem which can cause a failure to detect a leak of sensitive information. The variables x and y are both initialized to false. On Line 4, the attacker tests the user's input for a specific value. Let us assume that the attacker was lucky and the test was positive. In this case, Line 5 is executed, setting x to true and x is tainted. Variable y keeps its false value, since the assignment on Line 7 is not executed and y is not tainted because dynamic tainting occurs only along the branch that is actually executed. As y is not tainted, it is leaked to the network (Line 8) without being detected. Since y has not been modified, it informs the attacker about the value of the user private contact. Thus, an attacker can circumvent an android system through the control flows. In a previous work [START_REF] Graa | Detecting control flow in smarphones: Combining static and dynamic analyses[END_REF], we have proposed an approach that combines static and dynamic taint analysis to propagate taint along control dependencies and to track implicit flows in embedded systems such as the Google Android operating system. In this paper, we formally specify the under-tainting problem and we provide an algorithm to solve it based on a set of formally defined rules describing the taint propagation. We prove the completeness of those rules and the correctness and completeness of the algorithm.

The rest of this paper is organized as follows. Section 2 gives a technical overview of our approach. Section 3 presents some definitions and theorems that are used in other sections. Section 4 describes our formal specification of the under-tainting problem. In section 5, we specify an algorithm based on a set of formally defined rules describing the taint propagation policy that we use to solve the under-tainting problem. Related work about existing solutions to solve the under-tainting problem is analyzed in section 6. Finally, section 7 concludes with an outline of future work. II. APPROACH OVERVIEW TaintDroid [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF], an extension of the Android mobilephone platform, implements dynamic taint analysis to track the information flow in real-time and control the handling of private data. It addresses different challenges specific to mobile phones like the resource limitations. TaintDroid is composed of four modules: (1) Explicit flow module that tracks variable at the virtual machine level, (2) IPC Binder module that tracks messages between applications, (3) File module that tracks files at the storage level and (4) Taint propagation module that is implemented in the native methods level. It only tracks explicit flows and does not track control flows. In a previous work [START_REF] Graa | Detecting control flow in smarphones: Combining static and dynamic analyses[END_REF], we have proposed a technical approach that enhances the TaintDroid approach by tracking control flow in the Android system to solve the under-tainting problem. To track implicit flow, we have added an implicit flow module in the Dalvik VM bytecode verifier which checks instructions of methods at load time. We have defined two additional rules to propagate taint in the control flow. At class load time, we have built an array of variables to which a value is assigned to handle the branch that is not executed. Figure 2 presents the modified architecture to handle implicit flow in TaintDroid system. In this paper, we prove the completeness of the two additional rules and we provide a correct and complete taint algorithm based on these rules. Our algorithm is based on a hybrid approach that combines and benefits from the advantages of static and dynamic analyses. We use static analysis to detect control dependencies. This analysis is based on the control flow graphs [START_REF] Aho | Compilers: principles, techniques, and tools[END_REF], [START_REF]Control flow analysis[END_REF] which will be analyzed to determine branches in the conditional structure. A basic block is assigned to each control flow branch. Then, we detect the flow of the condition-dependencies from blocks in the graph. Also, we detect variable assignment in a basic block of the control flow graph to handle not executed branches. The dynamic analysis uses information provided by the static analysis and allows tainting variables to which a value is assigned in the conditional instruction. To taint these variables, we create an array of context taints that includes all condition taints. We use the context taints array and the conditiondependencies from block in the graph to set the context taint of each basic block. Finally, we apply the propagation rules to taint variables to which a value is assigned whether the branch is taken or not.

III. NOTATIONS, DEFINITIONS AND THEOREMS Definition 1. Direct graph

A directed graph G = (V, E) consists of a finite set V of vertices and a set E of ordered pairs (v, w) of distinct vertices, called edges. If (v, w) is an edge, w is a successor of v and v is a predecessor of w.

Definition 2. Complete directed graph

A complete directed graph is a simple directed graph G = (V, E) such that every pair of distinct vertices in G are connected by exactly one edge. So, for each pair of distinct vertices, either (x, y) or (y, x) (but not both) is in E.

Definition 3. Control flow graph

A control flow graph G = (V, E, r) is a directed graph (V, E) with a distinguished Exit vertex and start vertex r, such that for any vertex v ∈ V there is a path from r to v. The nodes of the control flow graph represent basic blocks and the edges represent control flow paths.

The concept of post-dominator and dominator tree are used to determine dependencies of blocks in the control flow graph. Theorem 1. Every vertex of a flow graph G = (V, E, r) except r has a unique immediate dominator. The edges {(idom(w), w)|w ∈ V -{r}} form a directed tree rooted at r, called the dominator tree of G, such that v dominates w if and only if v is a proper ancestor of w in the dominator tree [START_REF] Alfred | The theory of parsing, translation, and compiling[END_REF], [START_REF] Lowry | Object code optimization[END_REF].

Computing post-dominators in the control flow graph is equivalent to computing dominators [START_REF] Aho | Compilers: principles, techniques, and tools[END_REF] in the reverse control flow graph. Dominators in the reverse graph can be computed quickly by using the Fast Algorithm [START_REF] Lengauer | A fast algorithm for finding dominators in a flowgraph[END_REF] or a linear-time dominators algorithm [START_REF] Georgiadis | Finding dominators revisited[END_REF] to construct the dominator tree. Using these algorithms, we can determine the post-dominator tree of a graph. We use the completeness theorem to prove the completeness of the taint propagation rules in section V-A. We use the soundness theorem to prove this completeness from left to right and the compactness theorem and theorem 2 to prove from right to left. These theorems [START_REF] Hedman | A First Course In Logic: An Introduction To Model Theory, Proof Theory, Computability, And Complexity, Number n 9 in Oxford Texts in Logic[END_REF] are given below.

Completeness Theorem. For any sentence G and set of sentences F, F |= G if and only if F G.

Soundness Theorem. For any formula G and set of formulas

F, if F G, then F |= G.
Compactness Theorem. Let F be a set of formulas. F is unsatisfiable if and only if some finite subset of F is unsatisfiable.

Definition 8. CNF formula

A formula F is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals. That is, F = n i=1 ( m j=1 L i,j )
where each L i,j is either atomic or a negated atomic formula.

Theorem 2. Let F and G be formulas of the first-order logic. Let H be the CNF formula obtained by applying the CNF algorithm [START_REF] Hedman | A First Course In Logic: An Introduction To Model Theory, Proof Theory, Computability, And Complexity, Number n 9 in Oxford Texts in Logic[END_REF] to the formula F ∧ ¬G. Let Res * (H) be the set of all clauses that can be derived from H using resolvents. The following are equivalent:

1

) F |= G 2) F G 3) ∅ ∈ Res * (H)
IV. THE UNDER-TAINTING PROBLEM In this section we formally specify the under-tainting problem based on Denning's information flow model. Denning [START_REF] Denning | A lattice model of secure information flow[END_REF] defined an information flow model as:

F M =< N, P, SC, ⊕, →> .
N is a set of logical storage objects (files, program variables, ...). P is a set of processes that are executed by the active agents responsible for all information flow. SC is a set of security classes that are assigned to the objects in N . SC is finite and has a lower bound L attached to objects in N by default. The class combining operator "⊕" specifies the class result of any binary function on values from the operand classes. A flow relation "→" between pairs of security classes A and B means that "information in class A is permitted to flow into class B". A flow model F M is secure if and only if execution of a sequence of operations cannot produce a flow that violates the relation "→".

We draw our inspiration from the Denning information flow model to formally specify under-tainting. However, we assign taint to the objects instead of assigning security classes. Thus, the class combining operator "⊕" is used in our formal specification to combine taints of objects.

Syntactic definition of connectors {⇒, →, ←, ⊕}:

We use the following syntax to formally specify undertainting: A and B are two logical formulas and x and y are two variables.

• A ⇒ B : If A then B • x → y : Information flow from object x to object y • x ← y : the value of y is assigned to x • T aint(x) ⊕ T aint(y) : specifies the taint result of combined taints. Semantic definition of connectors {→, ←, ⊕}:

• The → connector is reflexive: If x is a variable then x → x. • The → connector is transitive: x, y and z are three variables, if (x → y) ∧ (y → z) then x → z. • The ← connector is reflexive: If x is a variable then x ← x. • The ← connector is transitive: x, y and z are three variables, if (x ← y) ∧ (y ← z) then x ← z. • The → and ← connectors are not symmetric. • The ⊕ relation is commutative: T aint(x) ⊕ T aint(y) = T aint(y) ⊕ T aint(x) • The ⊕ relation is associative: T aint(x)⊕(T aint(y)⊕ T aint(z)) = (T aint(x) ⊕ T aint(y)) ⊕ T aint(z) Definition 9. Under-Tainting
We have a situation of under-tainting when x depends on a condition, the value of x is assigned in the conditional branch and condition is tainted but x is not tainted.

Formally, an under-tainting occurs when there is a variable x and a formula condition such that:

IsAssigned(x, y) ∧ Dependency(x, condition) ∧T ainted(condition) ∧ ¬T ainted(x) (1)
where:

• IsAssigned(x, y) associates with x the value of y.

IsAssigned(x, y) def ≡ (x ← y)
• Dependency(x, condition) defines an information flow from condition to x when x depends on the condition.

Dependency(x, condition)

def

≡ (condition → x)
V. THE UNDER-TAINTING SOLUTION In this section, we specify a set of formally defined rules that describe the taint propagation. We prove the completeness of these rules. Then, we provide an algorithm to solve the under-tainting problem based on these rules. Afterwards, we analyse some important properties of our algorithm such as Correctness and Completeness.

A. The taint propagation rules

Let us consider the following axioms:

(x → y) ⇒ (T aint(y) ← T aint(x)) (2)
(x ← y) ⇒ (y → x) (3)
(T aint(x) ← T aint(y)) ∧ (T aint(x) ← T aint(z)) ⇒ (T aint(x) ← T aint(y) ⊕ T aint(z)) (4)
Theorem 3. We consider that Context T aint is the taint of the condition. To solve the under-tainting problem, we use the two rules that specify the propagation taint policy:

• Rule 1: if the value of x is modified and x depends on the condition and the branch is taken, we will apply the following rule to taint x.

IsM odif ied(x, explicitf lowstatement) ∧(Dependency(x, condition)) ∧(BranchT aken(br, conditionalstatement))

(T aint(x) ← Context T aint ⊕T aint(explicitf lowstatement))
where:

The predicate BranchT aken(br, conditionalstatement) specifies that branch br in the conditionalstatement is executed. So, an explicit flow which contains x is executed. IsModified (x, explicitflowstatement) associates with x the result of an explicit flow statement.

IsM odif ied(x, explicitf lowstatement) def ≡ (x ← explicitf lowstatement)
• Rule 2: if the value of y is assigned to x and x depends on the condition and the branch br in the conditional statement is not taken (x depends only on implicit flow and does not depend on explicit flow), we will apply the following rule to taint x.

IsAssigned(x, y) ∧ Dependency(x, condition) ∧¬BranchT aken(br , conditionalstatement) T aint(x) ← T aint(x) ⊕ Context T aint

Proof of taint propagation rules

To prove completeness of propagation taint rules, we use the basic rules cited in Table I for derivations. We prove soundness, left to right, by induction. If F G, then there is a formal proof concluding with F G (see Table II). Let M be an arbitrary model of applied to 3 and 6

Premise Conclusion Name G is in F F G Assumption F G and F ⊂ F F G Monotonicity F F ,F G F (F ∧ G) ∧-Introduction F (F ∧ G) F (G ∧ F ) ∧-Symmetry
F, we will demonstrate that M |= G. G is deduced by Modus ponens of G j , G j → G then by induction, M |= G j and M |= G j → G and it follows M |= G. Statement Justification 1. (condition → x) (T aint(x) ← T aint(condition)) Axiom (2)

8.F G

Modus ponens

Table II FORMAL PROOF OF THE FIRST RULE

Conversely, suppose that F |= G, then F ∪ ¬G is unsatisfiable. By compactness, some finite subset of F ∪ ¬G is unsatisfiable. So there exists finite F 0 ⊂ F such that F 0 ∪ ¬G is unsatisfiable and, equivalently, F 0 |= G. Since F 0 is finite, we can apply Theorem 2 to get F 0 G. Finally, F G by Monotonicity.

We will now prove completeness of the second rule. We assume again that F = {IsAssigned(x, y), Dependency(x, condition), ¬BranchT aken(br , conditionalstatement)} and G = T aint(x) ← T aint(x) ⊕ Context T aint.

Similarly to the first rule, we prove soundness by induction. If F G, then there is a formal proof concluding with F G (see Table III). applied to 8

10.F G

Modus ponens

Table III FORMAL PROOF OF THE SECOND RULE

Conversely, suppose that F |= G. Then F ∪ ¬G is unsatisfiable. By compactness, some finite subset of F ∪ ¬G is unsatisfiable. So there exists finite F 0 ⊂ F such that F 0 ∪ ¬G is unsatisfiable and, equivalently, F 0 |= G. Since F 0 is finite, we can apply Theorem 2 to get F 0 G. Finally, F G by Monotonicity.

B. The algorithm

The tainting algorithm that we propose, T aint Algorithm, allows solving the under-tainting problem. It takes as input a control flow graph of a binary program. In this graph, nodes represent a set of instructions that represent basic blocks. Firstly, it determines the control dependency of the different blocks in the graph using Dependency Algorithm [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF]. Afterwards, we parse the Dependency List generated by Dependency Algorithm and we set the context taint of blocks to include the taint of the condition that depends on whether the branch is taken or not. Finally, using the context taint and the two propagation rules, we taint all variables to which a value is assigned in the conditional branch.

C. Running example

We analyze the control flow graph G = (V, E, r) (see Figure 5) of the bytecode given in Figure 4 to illustrate the operation of the T aint Algorithm. The source code is given in Figure 3. The T aint Algorithm takes as input the control flow graph G = (V, E, r) where :

• V = {BB(

D. Properties of the algorithm

First, we prove the correctness of the T aint Algorithm and then we prove its completeness.

1) Correctness:

We want to prove the correctness of the T aint Algorithm. Let us assume that the control flow graph is correct [START_REF] Amighi | Provably correct control-flow graphs from java programs with exceptions[END_REF]. The proof consists of three steps: first prove that Dependency Algorithm is correct, then prove that Set Context T aint is correct, and finally prove that T aint Assigned V ariable is correct. Each step relies on the result from the previous step.

Correctness proof for Dependency Algorithm

The Dependency Algorithm is defined by Ferrante et al. [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF] to determine dependency of blocks in the graph. This algorithm takes as input the post-dominator tree for an augmented control flow graph (ACFG). Ferrante et al. add to the control flow graph a special predicate node ENTRY that has one edge labeled 'T' going to START node and another edge labeled 'F' going to STOP node. ENTRY corresponds to whatever external condition causes the program to begin execution. The post-dominator tree of ACFG can be created using the algorithms defined in [START_REF] Lengauer | A fast algorithm for finding dominators in a flowgraph[END_REF], [START_REF] Georgiadis | Finding dominators revisited[END_REF]. These algorithms are proven to be correct. Basic steps in the Dependency Algorithm:

Given the post-dominator tree, Ferrante et al. [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF] determine control dependencies as following:

• Find S,a set of all edges (A, B) in the ACFG such that B is not an ancestor of A in the post-dominator tree (i.e., B does not postdominate A). • For each edge (A, B) in S, find L, the least common ancestor of A and B in the post-dominator tree.

CLAIM: Either L is A or L is the parent of A in the post-dominator tree.

Ferrante et al. consider these two cases for L, and show that one method of marking the post-dominator tree with the appropriate control dependencies accommodates both cases.

-Case 1. L = parent of A. All nodes in the post-dominator tree on the path from L to B, including B but not L, should be made control dependent on A. -Case 2. L = A. All nodes in the post-dominator tree on the path from A to B, including A and B, should be made control dependent on A.

• Given (A, B) in S and its corresponding L, the algorithm given by Ferrante et al. traverses backwards from B in the post-dominator tree until they reach L and mark all nodes visited; mark L only if L = A. • Statements representing all marked nodes are control dependent on A with the label that is on edge (A, B). They prove that the correctness of the construction follows directly from the definition of control dependency (see section III).

Referring back to this definition, for any node M on the path in the post-dominator tree from (but not including) L to B, (1) there is a path from A to M in the control flow graph that consists of nodes post-dominated by M , and (2) A is not post-dominated by M . Condition (1) is true because the edge (A, B) gives us a path to B, and B is post-dominated by M . Condition (2) is true because A is either L, in which case it post-dominates M , or A is a child of L not on the path from L to B.

We can therefore conclude that Dependency Algorithm is correct.

Correctness proof for Set Context T aint

We include the taint of the condition in the context taint of the dependent blocks. As the condition taint is valid thus the inclusion operation is valid. We can conclude that Set Context T aint is correct.

Correctness proof for T aint Assigned V ariable

We use the two propagation rules to taint variables to which a value is assigned. We proved the completeness of the two propagation rules in section V-A, thus we can conclude that T aint Assigned V ariable is complete. Therefore, we can conclude the completeness of the T aint Algorithm.

2) Completeness: Let us assume that the control flow graph is complete (see Definition 2). To prove the completeness of the T aint Algorithm, we will prove the completeness of Dependency Algorithm and T aint Assigned V ariable.

The Dependency Algorithm takes as input the postdominator tree of the control flow graph. The postdominator tree can be constructed using the complete algorithm defined in [START_REF] Georgiadis | Finding dominators revisited[END_REF]. The Dependency Algorithm is based on the set of the least common ancestor (L) of A and B in the post-dominator tree for each edge (A, B) in S. According to the value of L, Ferrante et al. define two cases to determine the control dependency. To prove the completeness of the Dependency Algorithm, we show that Ferrante et al. prove that there does not exist another value of L (either A s parent or A itself) to consider. Proof: Let us assume that X is the parent of A in the post-dominator tree. So, X is not B because B is not an ancestor of A in the post-dominator tree (by construction of S). Ferrante et al. perform a proof reductio ad absurdum to demonstrate that X post-dominates B, and suppose it does not. Thus, there would be a path from B to ST OP that does not contain X. But, by adding edge (A, B) to this path, a path from A to ST OP does not pass through X (since, by construction, X is not B). This contradicts the fact that X post-dominates A. Thus, X post-dominates B and it must be an ancestor of B in the post-dominator tree. If X, immediate post-dominator of A, post-dominates B, then the least common ancestor of A and B in the postdominator tree must be either X or A itself.

As only two values of L exist, there does not exist another case to compute the control dependency. The Case 2 captures loop dependency and all other dependencies are determined according to Case 1. Thus, Dependency Algorithm is complete.

We proved the completeness of the two propagation rules in section V-A thus we can conclude that T aint Assigned V ariable is complete. Therefore, we can conclude the completeness of the Taint Algorithm.

E. Time complexity of the algorithm

The Dependency Algorithm performs with a time of at most O(N 2 ) where N is the number of nodes in the control flow graph. Linear time algorithm to calculate control dependencies have been proposed in [START_REF] Johnson | Dependence-based program analysis[END_REF] but no proof of correctness of this algorithm was given. For each (X, Y) examined in the Dependency List, setting context taint and tainting variables can be done in constant time O(N ). Thus, the T aint Algorithm requires linear time using algorithm defined in [START_REF] Johnson | Dependence-based program analysis[END_REF] and at most O(N 2 ) using Ferrante et al. algorithm.

VI. RELATED WORK

Privacy issues on smartphones are a growing concern. Several works [START_REF] Enck | On lightweight mobile phone application certification[END_REF], [START_REF] Nauman | Apex: extending android permission model and enforcement with user-defined runtime constraints[END_REF], [START_REF] Conti | Crepe: Context-related policy enforcement for android[END_REF], [START_REF] Bugiel | Practical and lightweight domain isolation on android[END_REF], [START_REF] Ongtang | Porscha: Policy oriented secure content handling in android[END_REF] have been proposed to control access to private data in mobile operating systems. These access control approaches do not track the flow of information and cannot prevent leakage of sensitive data. A number of researches have been proposed to prevent private information leakage by untrusted android applications. [START_REF] Zhou | Taming information-stealing smartphone applications (on android)[END_REF], [START_REF] Alastair R Beresford | Mockdroid: trading privacy for application functionality on smartphones[END_REF], [START_REF] Hornyack | These aren't the droids you're looking for: retrofitting android to protect data from imperious applications[END_REF] substitute private data by fake information in the data flow. This can cause a problem and disrupt execution of applications. Enck et al. [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF] implement dynamic taint analysis to track explicit flows on smartphones. AppFence [START_REF] Hornyack | These aren't the droids you're looking for: retrofitting android to protect data from imperious applications[END_REF] extends Taintdroid to implement enforcement policies. One limit of these approaches is that they cannot detect control flows because they use dynamic taint analysis. The static analysis approaches implemented in smartphones [START_REF] Egele | Pios: Detecting privacy leaks in ios applications[END_REF], [START_REF] Chin | Analyzing inter-application communication in android[END_REF], [START_REF] Adam P Fuchs | Scandroid: Automated security certification of android applications[END_REF] allow detecting data leaks but they cannot capture all runtime configuration and input. We were inspired by these prior works, but we combine static and dynamic analysis to prevent sensitive information leakage by untrusted android applications. Some implementations exist in the literature to solve the under-tainting problem. BitBlaze [START_REF] Song | Bitblaze: A new approach to computer security via binary analysis[END_REF] presents a novel fusion of static and dynamic taint analysis techniques to track implicit and explicit flow. DTA++ [START_REF] Kang | Dta++: Dynamic taint analysis with targeted control-flow propagation[END_REF], based on the Bitblaze approach, presents an enhancement of dynamic taint analysis to limit the undertainting problem. However DTA++ is evaluated only on benign applications but malicious programs in which an adversary uses implicit flows to circumvent analysis are out of scope. Trishul [START_REF] Nair | A virtual machine based information flow control system for policy enforcement[END_REF] correctly identifies implicit flow of information to detect a leak of sensitive information. Egele et al. [START_REF] Egele | Dynamic spyware analysis[END_REF] associate a taint label with the program counter to enhance dynamic taint-tracking technique. They identify unknown components like spyware and provide comprehensive reports on their behavior. Furthermore, these approaches do not formally give a proof to solve the under-tainting problem and are not implemented in smartphones application. Fenton [START_REF] Fenton | Memoryless subsystem[END_REF] proposed a Data Mark Machine, an abstract model, to handle control flows. Fenton associates a security class to information and defines an interaction matrix to manipulate data in the system. He gives a formal description of his model and a proof of its correctness in terms of information flow. The Data Mark Machine is based on a runtime mechanism that does not take into account the implicit flow when the branch is not executed. This can cause an under-tainting problem. To solve this problem, Aries [START_REF] Brown | A minimal trusted computing base for dynamically ensuring secure information flow[END_REF] considers that writing to a particular location within a branch is disallowed when the security class associated with that location is equal or less restrictive than the security class of program counter. The Aries approach is based only on high and low security classes. Denning [START_REF] Denning | Secure information flow in computer systems[END_REF] enhances the run time mechanism used by Fenton with a compile time mechanism to solve the under-tainting problem. Denning inserts updating instructions whether the branch is taken or not to reflect the information flow. Denning and Denning [START_REF] Denning | Certification of programs for secure information flow[END_REF] gave an informal argument for the soundness of their compile time mechanism. Graa et al. [START_REF] Graa | Detecting control flow in smarphones: Combining static and dynamic analyses[END_REF] propose an approach based on dynamic taint analysis that propagates taint along control dependencies using static analysis to track implicit flows in embedded systems such as the Google Android operating system. They define a set of formal propagation rules to solve the under-tainting problem but they do not prove the completness of these rules. We draw our inspiration from the Denning approach, but we define formally a set of taint propagation rules to solve the under-tainting problem and we improve the approach of Graa et al. by proving the correctness and completeness of these rules.

VII. DISCUSSION

Cavallaro et al. [START_REF] Cavallaro | On the limits of information flow techniques for malware analysis and containment[END_REF] describe evasion techniques that can easily defeat dynamic information flow analysis. These evasion attacks can use control dependencies. They demonstrate that a malware writer can propagate an arbitrarily large amount of information through control dependencies. Cavallaro et al. see that it is necessary to reason about assignments that take place on the unexecuted program branches. We implement the same idea in our taint propagation rules. Unfortunately, this will lead to an over-tainting problem (false positives). The problem has been addressed in [START_REF] Kang | Dta++: Dynamic taint analysis with targeted control-flow propagation[END_REF] and [START_REF] Bao | Strict control dependence and its effect on dynamic information flow analyses[END_REF] but not solved though. Kang et al. [START_REF] Kang | Dta++: Dynamic taint analysis with targeted control-flow propagation[END_REF] used a diagnosis technique to select branches that could be responsible for undertainting and propagated taint only along these branches in order to reduce over-tainting. However a smaller amount of over tainting occurs even with DTA++, as we can see by comparing the "Optimal" and "DTA++" results in the evaluation. Bao et al. [START_REF] Bao | Strict control dependence and its effect on dynamic information flow analyses[END_REF] define the concept of strict control dependencies (SCDs) and introduce its semantics. They use a static analysis to identify predicate branches that give rise to SCDs. They do not consider all control dependencies to reduce the number of false positives. Their implementation gives similar results as DTA++ in many cases, but is based on the syntax of a comparison expression. Contrariwise, DTA++ uses a more general and precise semantic-level condition, implemented using symbolic execution.

In our approach, we taint all variables in the conditional branch. This causes an over-tainting. But it provides more security because all confidential data are tainted. So, the sensitive information cannot be leaked. We are interested in solving the under tainting because the false negatives are much more dangerous than the false positives since the false negatives can lead to a false sense of security. We can try to reduce the over-tainting problem by considering expert rules.

VIII. CONCLUSION

Smartphones are extensively used. However, the use of untrusted android applications can provoke the leakage of private data by exploiting the under-tainting problem. In this paper, we propose a formal approach to detect control flow and to solve the under-tainting problem in android sytem. We formally specify the under-tainting problem. As a solution, we provide an algorithm based on a set of formally defined rules that describe the taint propagation. We prove the completeness of those rules and the correctness and completeness of the algorithm. In the future works, we will evaluate our approach in terms of overhead and false alarms. We will also test our approach and show that it resists to code obfuscation attacks based on control dependencies.

Figure 1 .

 1 Figure 1. Attack using indirect control dependency

Figure 2 .

 2 Figure 2. Modified architecture to handle implicit flow in TaintDroid system.

Definition 4 .

 4 Dominator A vertex v dominates another vertex w = v in G if every path from r to w contains v. Definition 5. Post-Dominator A node v is post-dominated by a node w in G if every path from v to Exit (not including v) contains w.

Definition 6 . 2 )

 62 Control Dependency Let G be a control flow graph. Let X and Y be nodes in G. Y is control dependent on X noted Dependency(X, Y ) if:1) There exists a directed path P from X to Y with any Z in P (excluding X and Y ) post-dominated by Y and X is not post-dominated by Y . Given the post-dominator tree, Ferrante et al.[START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF] determine control dependencies by examining certain control flow graph edges and annotating nodes on the corresponding tree paths. Definition 7. Context Taint Let G be a control flow graph. Let X and Y be basic blocks in G. If Y is control dependent on X that contains Condition then we associate to Y a Context T aint with Context T aint(Y ) = T aint(Condition).

2 .(explicitf lowstatement → x) 5 .

 25 (condition → x) (T aint(x) ← Context T aint) (x ← explicitf lowstatement) Axiom (2) (T aint(x) ← T aint(explicitf lowstatement)) 6. F (T aint(x) ← T aint(explicitf lowstatement))Monotonicity applied to 5 7. F ((T aint(x) ← Context T aint)∧ ∧-Introduction (T aint(x) ← T aint(explicitf lowstatement)))

Axiom ( 2 ) 2 .

 22 Let M be an arbitrary model of F, we will demonstrate that M |= G. G is deduced by Modus ponens ofG j , G j → G then by induction, M |= G j and M |= G j → G and it follows M |= G. Statement Justification 1. (condition → x) (T aint(x) ← T aint(condition)) (condition → x) (T aint(x) ← Context T aint) aint(x) ← Context T aint)∧ ∧-Introduction (T aint(x) ← T aint(x))) aint(x) ← T aint(x))∧∧-Symmetry(T aint(x) ← Context T aint))

Algorithm 1

 1 Taint Algorithm (Control flow graph G) Input: G = (V, E, r) is a control flow graph of a binary program Output: T ainted V ariables List is the list of variables that are tainted. x ∈ V y ∈ V Dependency List ← Dependency Algorithm(G) while (x, y) ∈ Dependency List do Set Context T aint(y, List Context T aint) T ainted V ariables List ← T aint Assigned V ariable(y) end while

Figure 3 .

 3 Figure 3. Source code example Figure 4. Bytecode example

  1), BB(2), BB(3), BB(4)} • E = {(BB(1), BB(2)), (BB(1), BB(3)), (BB(2), BB(4)), (BB(3), BB(4))} • r = {BB(1)} The Dependency Algorithm checks the dependency of the blocks in the control flow graph. It generates a Dependency List = {(BB(1), BB(2)); (BB(1), BB(3))}. As, BB(2) depends on BB(1) and BB(3) depends on BB(1), the T aint Algorithm sets context taint of BB(2) and context taint of BB(3) to condition taint in BB(1). If x = true, the first branch is executed but the second is not. The first rule is used to taint modified variable y in BB(2) : T aint(y) = ContextT aint ⊕ T aint(explicitf lowstatement).The second rule is used to taint the variable y in BB(3) : T aint(y) = ContextT aint ⊕ T aint(y). So, all variables that depend on the condition will be tainted and stored in T ainted V ariables List whether the branch is taken or not and we do not have an under-tainting problem.

Figure 5 .

 5 Figure 5. Control flow graph corresponding to the example given in Figure 3.


Truong-Giang Le
email: le-truong.giang@isep.fr

Dmitriy Fedosov

Olivier Hermant
email: olivier.hermant@mines-paristech.fr

Matthieu Manceny
email: matthieu.manceny@isep.fr

Renaud Pawlak
email: renaud.pawlak@gmail.com

Renaud Rioboo
email: renaud.rioboo@ensiie.fr

Programming Robots with Events

Keywords: robotics, event-based programming, context-aware reactive systems, parallel programming

We introduce how to use event-based style to program robots through the INI programming language. INI features both built-in and user-defined events, a mechanism to handle various kinds of changes happening in the environment. Event handlers run in parallel either synchronously or asynchronously, and events can be reconfigured at runtime to modify their behavior when needed. We apply INI to the humanoid robot called Nao, for which we develop an object tracking program.

Introduction

The word "robot" was coined by the Czech novelist Karel Capek in a 1920 play titled Rassum's Universal Robots. In Czech, "robot" means worker or servant. According to the definition of the Robot Institute of America dating back to 1979, robot is: A reprogrammable, multifunctional manipulator designed to move material, parts, tools or specialized devices through variable programmed motions for the performance of a variety of tasks.

At present, people require more from the robots, since they are considered as a subset of "smart structures" -engineered constructs equipped with sensors to "think" and to adapt to the environment [START_REF] Wadhawan | Robots of the future[END_REF]. Generally, robots can be put into three main categories: manipulators, mobile robots and humanoid robots [START_REF] Russell | Artificial Intelligence: A Modern Approach[END_REF].

Robots now play an important role in many domains. In manufacturing, robots are used to replace humans in remote, hard, unhealthy or dangerous work. They will change the industry by replacing the CNC (Computer(ized) Numerical(ly) Control(led)) machines. In hospitals, they are employed to take care of the patients, and even do complex work like performing surgery. In education, robots may be good assistants for the children. They maybe also good friends for old people at home for talking and sharing housework. The global service robotics market in 2011 was worth $18.39 billion. This market is valued at $20.73 billion in 2012 and expected to reach $46.18 billion by 2017 at an estimated CAGR (Compound Annual Growth Rate) of 17.4% from 2012 to 2017 [START_REF]M&M: Service robotics market (personal & professional) global forecast & assessment by applications & geography[END_REF]. As a result, research on robot gets an increasing interests from governments, companies, and researchers [START_REF] Bar-Cohen | The Coming Robot Revolution: Expectations and Fears About Emerging Intelligent, Humanlike Machines[END_REF][START_REF] Bekey | Robotics: State of the Art and Future Challenges[END_REF].

Building a robot program is a complex task since a robot needs to quickly react to variabilities in the execution environment. In other words, a robot should be indeed autonomous. Besides, it should be able to do several things at one time. Consequently, using a programming language or development framework dedicated to robots is essential. The ultimate goal is to help programmers develop robot programs more efficiently and straightforwardly.

We give an overview of such robot programming languages and frameworks in Section 2. Next, in Section 3, we discuss how to define and apply events in our novel programming language called INI, especially its advanced features like events synchronization and reconfiguration. Then, we present a case study of using INI to control the humanoid robot Nao to track an object (Section 4). Finally, some conclusions and future work are discussed in Section 5.

Related Work

Classical languages like Java, C/C++, .Net are usually used for programming robot [START_REF] Auyeung | Robot programming in C[END_REF][START_REF] Kang | Robot Development Using Microsoft Robotics Developer Studio[END_REF][START_REF] Preston | The Definitive Guide to Building Java Robots (The Definitive Guide to)[END_REF]. However, developing robot's applications using these languages require more time and effort since they are not fully dedicated to this purpose. For example, to support interaction between robots and environment when something happens, programmers have to construct a mechanism for event detection and handling. In order to do this, programmers need to write a lot of code or may use some extensions like [START_REF] Jayaram | Context-oriented programming with EventJava[END_REF]23] although they are not easy to adapt.

Additionally, several robotic development platforms and DSLs (Domain Specific Languages) have been designed to assist programmers. Urbiscript is a scripting language primarily designed for robotics. It's a dynamic, prototype-based, and object-oriented scripting language. It supports and emphasizes parallel and event-based programming, which are very popular paradigms in robotics, by providing core primitives and language constructs [START_REF] Gostai | The Urbi Software Development Kit[END_REF]. UrbiScript has some limitations. First, it is an untyped language. Besides, it lacks support for synchronization among events, which is essential in some scenarios. Moreover, events in UrbiScript cannot be reconfigured at runtime to change their behavior.

The KUKA Robot Programming Language is developed by KUKA, one of the world's leading manufacturers of industrial robots [6]. KUKA is simple, Pascal-like and lacks many features. A Matlab abstraction layer has been introduced to extend its capabilities [START_REF] Chinello | Kuka control toolbox[END_REF]. RoboLogix is a scripting language that utilizes common commands, or instruction sets among major robot manufacturers. RoboLogix programs consist of data objects and a program flow [START_REF]Robologix[END_REF]. The data objects reside in registers and the program flow represents the list of instructions, or instruction set, that is used to program the robot. However, RoboLogix still does not supply a well-defined mechanism for the robots to interact and react to environment.

In recent years, event-driven programming has emerged as an efficient method for interacting and collaborating with the environment in ubiquitous computing. Using event-driven style requires less effort and may lead to more robust software [START_REF] Dabek | Event-driven programming for robust software[END_REF]. This style is used to write many kinds of applications: robotics, context-aware reactive applications, self-adaptive systems, interactive systems, etc. In consequence, several event-based programming languages have been developed so far [START_REF] Cohen | EventScript: an event-processing language based on regular expressions with actions[END_REF][START_REF] Holzer | Putting events in context: aspects for event-based distributed programming[END_REF]. However, in these languages, events still cannot be defined intuitively and straightforwardly, and their features are still limited. For example, events cannot run in parallel to take advantage of multiple processors. Besides, programmers may not dynamically customize events' behavior to deal with changes in the environment.

Considering limitations of current event-based programming language, we have developed a novel programming language called INI. With INI, developers may define and use events easily. Along with several built-in events, they also can write their own events in Java or in C/C++, and then integrate to INI programs. Events in INI may run concurrently either asynchronously or synchronously. Moreover, events may be reconfigured at run time to handle different scenarios happening in the context.

Event-Based Programming with INI

Overview

Events are used to monitor changes happening in the environment or for time scheduling. In other words, any form of monitoring can be considered to be compatible with event-based style. Generally, there are three types of events [START_REF] Mühl | Distributed Event-Based Systems[END_REF]:

-A timer event to express the passing of time.

-An arbitrary detectable state change in the system, e.g. the change of the value of a variable during execution. -A physical event such as the appearance of a person detected by cameras.

For example, programmers may define an event to monitor the power level of their systems or to observe users' behavior in order to react. They can also specify an event to schedule a desired action at preferable time. To understand more about event-based programming, please refer to [START_REF] Etzion | Event Processing in Action[END_REF][START_REF] Faison | Event-Based Programming: Taking Events to the Limit[END_REF].

INI is a programming language developed by ourselves, which runs on Java Virtual Machine (JVM) but INI's syntax and semantics are not Java's ones. INI is developed aiming at supporting the development of concurrent and contextaware reactive systems, which need a well-defined mechanism for capturing and handling events. As shown later, INI supports all those kinds of event. Event callback handlers (or events instances) are declared in the body of functions and are raised, by default asynchronously, every time the event occurs. By convention, an event instance in INI starts with @ and takes input and output parameters. Input parameters are configuration parameters to tune the event execution. Output parameters are variable names that are filled in with values when then the event callback is called, and executed in a new thread. They can be considered as the measured characteristic of the event instance. It has to be noticed that those variables, as well as any INI variable, enjoy a global scope in the function's body. Both kinds of parameters are optional. Moreover, an event can also be optionally bound to an id, so that other parts of the program can refer to it. The syntax of event instances is shown below:

id:@eventKind [inputParam1 =value1 , inputParam2 =value2 , ...] (outputParam1 , outputParam2 , ...) { <action > } Table 1. Some built-in events in INI
Built-in event kind Meaning @init() used to initialize variables, when a function starts. @end() triggered when no event handler runs, and when the function is about to return. @every[time:Integer]() occurs periodically, as specified by its input parameter (in milliseconds). @update[variable:T] invoked when the given variable's value changes (oldValue:T, newValue:T) during execution. @cron[pattern:String]() used to trigger an action, based on the UNIX CRON pattern indicated by its input parameter.

Programmers may use built-in events (listed in Table 1), or write user-defined events (in Java or in C/C++), and then integrate them to their INI programs through bindings. By developing custom events, one can process data which are captured by sensors. To illustrate events in INI, let's consider a program which uses sensors to capture and collect weather and climate data like humidity, temperature, wind speed, rainfall, etc. In our program, we can define separate events to handle these tasks as shown in Figure 1. For instance, we can define an event @humidityMonitor to observe the humidity level periodically. This event has one input parameter named humPeriod that sets the periodicity of the checks (time unit is in hours). Besides, it has one output parameter named humidity to indicate the current humidity. Inside this event, depending on the value of the current humidity, we can define several corresponding actions such as warning when the humidity is too high. Other events can be defined in a similar structure. The last event is a built-in @cron event, which is employed to send these data to a server at 3:00 AM, 11:00 AM, and 7:00 PM every day (to learn more about UNIX CRON pattern, please refer to [7]). All events in our program run in parallel so that it can handle multiple tasks at one time.

T.-G. Le et al.

Advanced Use of Events

By default, except for the @init and @end events (see Table 1), all INI events are executed asynchronously. However, in some scenarios, a given event e0 may want to synchronize on other events e1,..., eN. It means that the synchronizing event e0 must wait for all running threads corresponding to the target events to be terminated before running. For instance, when e0 may affect the actions defined inside other events, we need to apply the synchronization mechanism. The syntax corresponding to the above discussion is:

$(e1,e2,...,eN) e0:@eventKind [...](...) { <action > }

Events in INI may be reconfigured at runtime in order to adjust their behavior when necessary to adapt to changes happening in the environment. Programmers may use the built-in function reconfigure event(eventId, [inputParam1= value1, inputParam2=value2,...]) in order to modify the values of input parameters of the event referred to by eventId. For instance, in the example of Figure 1, we can call reconfigure event(h, [humPeriod=0.5]) to set the humidity data collection period to 30 minutes. Now our event will gather data every 30 minutes instead of one hour as before. Besides, we also allow programmers to stop and restart events with two built-in functions: stop event([eventId1, eventId2,...]) and restart event([eventId1, eventId2,...]). For example, we can stop all data collection processes when the energy level of the system is too low, and restart them later when the energy is restored. Last but not least, events in INI may be used in combination with a boolean expression to express the requirement that need to be satisfied before they can be executed. Programmers may use the syntax below:

<event_expression > <logical_expression > { <action > }
For example, if we want the event @humidityMonitor to be executed only when the temperature is higher than some threshold: @humidityMonitor [humPeriod =1]( humidity) temperature >... {...}

To understand more about the above mechanisms and other aspects of INI (e.g. developing user-defined events, rules, type system, type checking, and built-in functions), the readers may have a look at [START_REF] Le | Unifying event-based and rule-based styles to develop concurrent and context-aware reactive applications -toward a convenient support for concurrent and reactive programming[END_REF][START_REF] Truong-Giang | INI Online[END_REF].

A Case Study with the Humanoid Robot Nao

In this section, we briefly present the humanoid robot Nao, especially its features related to the moving mechanism. Then we show an INI tracking program running on Nao. The purpose of our INI program is controlling the Nao to detect a ball in the space and then walk to reach it.

Introduction to Nao and Its Moving Mechanism

Nao is the humanoid robot that is built by the French company Aldebaran-Robotics [START_REF] Gouaillier | The Nao humanoid: A combination of performance and affordability[END_REF]25]. It is equipped with many sensor devices to obtain robot's close environment information (see Figure 2). Nao has for instance become a standard platform for RoboCup, an international initiative that fosters research in robotics and artificial intelligence [START_REF] Federation | Robocup's homepage[END_REF]. NAOqi is the middleware running on Nao that helps prepare modules to be run either on Nao or on a remote PC. Code can be developed on Windows, Mac or Linux, and be called from many languages including C++, Java, Python and .Net. The company Aldebaran Robotics developed many modules built on top of this framework that offer rich APIs for interacting with Nao, including functionalities related to audio, vision, motion, communication or several lowlevel accesses. They also provide a well-organized documentation, particularly on how to control the robot effectively [24].

Nao is able to walk on multiple floor surfaces such as carpet, tiles and wooden floors. Each step is composed of a double leg and a single leg support phase. With Nao, the basic foot step planner is used by the walk process [24], provided by three possible walk control APIs: ALMotionProxy::setWalkTarget Velocity() (applied in our later case study), ALMotionProxy :: walkTo() or ALMotionProxy::setFootSteps(). The foot's position is specified by three parameters: x, y and θ (see Figure 3). x is the distance along the X axis in meters (forwards and backwards). y is the distance along the Y axis in meters (lateral motion). θ is the robot orientation relative to the current orientation (i.e. the rotation around the Z axis) in radians [-3.1415 to 3.1415]. The movement is composed of a translation by x and y, then a rotation around the vertical Z axis θ.Itis possible to define custom gait parameters for the walk of Nao so that we can control the direction and speed to adjust to different scenarios. To learn more about these parameters (e.g. MaxStepX, MaxStepY, MaxStepTheta, MaxStepFrequency, etc.) along with their value ranges and default values, please refer to Nao's documentation [24]. In INI, we abstract over many of those parameters through user-defined events and functions in order to facilitate programming.

An INI Tracking Program Running on Nao

In this part, we show how INI can be applied for programming robot through the example of building a ball tracking program. Figure 3 displays the possible relative positions between the robot and the ball. There are three distinguished zones that are specified based on the distance from the robot to the detected ball. And then according to which zone the ball belongs to, we can control the robot with the desired behavior:

-Zone 1: When the distance from the robot to the detected ball is larger than the forwardThreshold (unit is in meters and its range is 0.0 -1.0 meters), the ball is considered as far from the robot and it needs to move in order to reach the ball.

-Zone 2: When the distance from the robot to the detected ball is between backwardThreshold (its unit and range are the same as forwardThreshold) and forwardThreshold, the robot does not move since its place can be considered as a good position to observe the ball. However, the robot's head still can turn to continue to follow the ball. -Zone 3: When the distance from the robot to the detected ball is shorter than backwardThreshold, the ball is considered as too close and moving towards the robot. As a result, the robot will go backward in order to avoid the collision and keep its eyes on the ball.

The activity diagram of the strategy is shown in Figure 4. Our program is shown that then we can calculate appropriate needed direction and speed for its movement. stepX is the fraction (between 0.0 and 1.0) of MaxStepX (the maximum translation along the X axis for one step, see [24]). The sign of stepX also indicates the moving direction (forward or backward) of the Nao. The boolean variable needAdjustDirection is used to indicate whether we need to adjust the direction when the robot moves towards the ball. The intention of using the temporary variable i will be explained later.

The event @detectBall (lines 17-28) is a user-defined event written in Java, which uses image processing techniques to detect a ball with the help of video cameras located in the forehead of Nao. This event has three input parameters: robotIP , robotPort and checkingTime have the same meanings that the corresponding variables ip, port and interval described before own. Inside this event, when a ball is detected, we call the function process position to process positions of the ball and the robot, and also specify the appropriate direction and velocity for the robot's movement.

The event @every (lines 29-43) is applied to control the robot to move towards the target every 200 milliseconds. The function reach to target is used to determine a suitable velocity for the robot and to control the robot moving towards the ball. The robot only moves when all needed parameters related to orientation, velocity and frequency are specified. Each call of that function makes one walking step. During execution, the robot may adjust the direction and velocity to make them more well-suited since the ball may change its position. As a result, after each step when the robot comes to the new location, we calculate the direction error. If the error for θ exceeds the allowed threshold (e.g. 10 degrees), the variable needAdjustDirection becomes true and some adjustments will be applied so that the robot walks in the correct way. We use the temporary variable i to reset some parameters. When i>3 , this means that the robot already walked for three successful steps without checking again the position of the ball. In this case, by resetting some parameters, the robot will stop temporarily. Then it waits to detect the ball again to check whether during its displacement, the ball has moved to another place or not. If yes, Nao gets the updated position of the ball, then continues to walk and reach it.

In our program, we synchronize the two events @detectBall and @every in order to avoid data access conflicts and unwanted behavior. For example, the robot is controlled to walk to the ball only when all needed parameters are calculated. Besides, we want to ensure that during the calculation of parameters, the robot is not moving so that the measured numbers are correct and stable. Consequently, we add the notation for synchronization, i.e. $(...) before each event (line 17 and line 29). Additionally, the event @every is also synchronized with itself so that each robot step does not overlap with others.

When running in experiment, our program completes well the desired requirements. The robot detects the orange ball in the space and then follows it. When the ball is moved to another position, Nao also changes the direction and speed to reach the ball if needed. A demonstration video can be watched on YouTube [START_REF] Le | A demonstration video[END_REF].

Conclusion and Future Work

In this paper, we presented how to write robot applications by using INI, a novel programming language that supports event-based paradigm. Programmers may use built-in events, or develop custom events in other languages like Java or C/C++ and then integrate them to INI programs. Moreover, events may run in parallel (asynchronously or synchronously) to speed up the execution and improve performance. Last but not least, in case of changes happening in the environment, events can be dynamically reconfigured to adapt to a new context.

For future work, we will extend our example by adding more features to our program such as detecting and avoiding obstacles on the way to the target and control robot's hands to catch the object. We also have a plan to develop more practical applications running on Nao. For example, we can build a program which may recognize the human voice commands, and then control the robot to act the desired behavior.

G

  . Schirner et al. (Eds.): IESS 2013, IFIP AICT 403, pp. 14-25, 2013. c IFIP International Federation for Information Processing 2013

10 @ 11 / 12 } 13 }Fig. 1 .

 101112131 Fig. 1. A sample INI program used for collecting climate data

Fig. 2 .

 2 Fig. 2. Nao's features [25]

Fig. 3 .

 3 Fig. 3. Possible relative positions among the robot and the ball

Fig. 4 . 17 $Fig. 5 .

 4175 Fig. 4. The activity diagram for our program

Acknowledgments. The work presented in this article is co-funded by the European Union. Europe is committed in Ile-de-France with the European Regional Development Fund.