Android Security

may 2015

I am currently working on the security of Android applications and operating system. I investigate these objectives:

  • how to build attacks with different assumptions, for example that the application is malicious but is not root or that the attacker has compromised the operating system. The main attacks that I consider are the capture of some personal information of the user.
  • how to characterize malware: studying malware help to understand attackers' motivation. Malware analysis becomes a challenge because developers now include countermeasure to defeat dynamic analysis processes.
  • protection solutions: based on the two previous points, I try to elaborate countermeasures inside applications or at operating system level to defeat attacks.

GroddDroid: a tool for triggering of malware

The first video presents GroddDroid, a tool that tries to execute automatically Android malware. The originality of GroddDroid is that the tool tries to force the control flow in order to reach the branches where he thinks that suspicious code is hidden. GroddDroid has been awarded at MALWARE 2015 and is freely available on the Kharon project website.

Exfiltrating data with covert channels

The second video illustrates an attack that builds a covert channel between two applications. The first application, the CC collector, can access the personal data of the user. The second one, the CC sender, can access the internet. Building a covert channel between the two applications enables to make the personal information flow to the internet.

  • GroddDroid: A gorilla for triggering malicious behaviors
    A. Abraham, R. Andriatsimandefitra, A. Brunelat, J. F. Lalande, V. Viet Triem Tong
    2015 10th International Conference on Malicious and Unwanted Software, MALWARE 2015 MALWARE 2015 IEEE Computer Society 119-1272015 doi url
    Android malware authors use sophisticated techniques to hide the malicious intent of their applications. they use cryptography or obfuscation techniques to avoid detection during static analysis. they can also avoid detection during a dynamic analysis. frequently, the malicious execution is postponed as long as the malware is not convinced that it is running in a real smartphone of a real user. however, we believe that dynamic analysis methods give good results when they really monitor the malware execution. in this article, we propose a method to enhance the execution of the malicious code of unknown malware. we especially target malware that have triggering protections, for example branching conditions that wait for an event or expect a specific value for a variable before triggering malicious execution. in these cases, solely executing the malware is far from being sufficient. we propose to force the triggering of the malicious code by combining two contributions. first, we define an algorithm that automatically identifies potentially malicious code. second, we propose an enhanced monkey called grodddroid, that stimulates the gui of an application and forces the execution of some branching conditions if needed. the forcing is used by grodddroid to push the execution flow towards the previously identified malicious parts of the malware and execute it. the source code for our experiments with grodddroid is released as free software. we have verified on a malware dataset that we investigated manually that the malicious code is accurately executed by grodddroid. additionally, on a large dataset of 100 malware we precisely identify the nature of the suspicious code and we succeed to execute it at 28\%.
    (best paper award)
  • Analysis of Human Awareness of Security and Privacy Threats in Smart Environments
    Luca Caviglione, Jean-Francois Lalande, Wojciech Mazurczyk, Steffen Wendzel
    vol. 9190 3rd International Conference on Human Aspects of Information Security, Privacy and Trust HAS 2015 Springer Berlin / Heidelberg LNCS 165-1772015 doi url
    Smart environments integrate information and communication technologies (ict) into devices, vehicles, buildings and cities to offer an increased quality of life, energy efficiency and economical sustainability. in this perspective, the individual has a core role and so has networking, which enables such entities to cooperate. however, the huge amount of sensitive data, social aspects and the mixed set of protocols offer many opportunities to inject hazards, exfiltrate information, mass profiling of citizens, or produce a new wave of attacks. this work reviews the major risks arising from the usage of ict-techniques for smart environments, with emphasis on networking. its main contribution is to explain the role of different stakeholders for causing a lack of security and to envision future threats by considering human aspects.
  • Hiding privacy leaks in Android applications using low-attention raising covert channels
    Jean-François Lalande, Steffen Wendzel
    First International Workshop on Emerging Cyberthreats and Countermeasures ECTCM 2014 IEEE Computer Society 701-7102013 doi url
    Covert channels enable a policy-breaking communication not foreseen by a system's design. recently, covert channels in android were presented and it was shown that these channels can be used by malware to leak confidential information (e.g., contacts) between applications and to the internet. performance aspects as well as means to counter these covert channels were evaluated. in this paper, we present novel covert channel techniques linked to a minimized footprint to achieve a high covertness. therefore, we developed a malware that slowly leaks collected private information and sends it synchronously based on four covert channel techniques. we show that some of our covert channels do not require any extra permission and escape well know detection techniques like taintdroid. experimental results confirm that the obtained throughput is correlated to the user interaction and show that these new covert channels have a low energy consumption – both aspects contribute to the stealthiness of the channels. finally, we discuss concepts for novel means capable to counter our covert channels and we also discuss the adaption of network covert channel features to android-based covert channels.
  • Repackaging Android applications for auditing access to private data
    Pascal Berthomé, Thomas Fécherolle, Nicolas Guilloteau, Jean-François Lalande
    First International Workshop on Security of Mobile Applications IWSMA 2012 IEEE Computer Society 388-3962012 doi url
    One of the most important threats for android users is the collection of private data by malware put on the market. most of the proposed approaches that help to guarantee the user's privacy rely on modified versions of the android operating system. in this paper, we propose to automatically detect when an application accesses private data and to log this access in a third-party application. this detection should be performed without any modification to the operating system. the proposed methodology relies on the repackaging of a compiled application and the injection of a reporter at bytecode level. thus, such a methodology enables the user to audit suspicious applications that ask permissions to access private data and to know if such an access has occurred. we show that the proposed methodology can also be implemented as an ips, in order to prevent such accesses. experimental results show the efficiency of the methodology on a set of 18 regular applications of the android market that deal with contacts. our prototype detected 66\%of the accesses to the user's contacts. we also experimented the detection of privacy violations with 5 known malware that send premium-rate sms.

Privacy for mobile services

may 2015

I am also working on the problem of privacy when using mobile services. I am participating to the supervision of Ghada Arfaoui who is doing her PhD at Orange Labs (Caen). We designed two transport protocols that guarantee that a user using a smartphone to authenticate at a transport gate cannot be traced by the transport authority. The computation is protected in a smart card, even if some operations are delegated to the smartphone for efficiency purpose. We have developed a prototype that shows that the cryptographic protocol take advantage of the secure element and meets the functional constraints of transport operators, i.e. a validation occurs in less than 300 ms.

  • A Practical Set-Membership Proof for Privacy-Preserving NFC Mobile Ticketing
    Ghada Arfaoui, Jean-François Lalande, Jacques Traoré, Nicolas Desmoulins, Pascal Berthomé, Saïd Gharout
    Proceedings on Privacy Enhancing Technologies vol. 2015 2 PoPETS De Gruyter Open 25-452015 doi url
    To ensure the privacy of users in transport systems, researchers are working on new protocols providing the best security guarantees while respecting functional requirements of transport operators. in this paper1, we design a secure nfc m-ticketing protocol for public transport that preserves users' anonymity and prevents transport operators from tracing their customers' trips. to this end, we introduce a new practical set-membership proof that does not require provers nor verifiers (but in a specific scenario for verifiers) to perform pairing computations. it is therefore particularly suitable for our (ticketing) setting where provers hold sim/uicc cards that do not support such costly computations. we also propose several optimizations of boneh-boyen type signature schemes, which are of independent interest, increasing their performance and efficiency during nfc transactions. our m-ticketing protocol offers greater flexibility compared to previous solutions as it enables the post-payment and the off-line validation of m-tickets. by implementing a prototype using a standard nfc sim card, we show that it fulfils the stringent functional requirement imposed by transport operators whilst using strong security parameters. in particular, a validation can be completed in 184.25ms when the mobile is switched on, and in 266.52ms when the mobile is switched off or its battery is flat.
  • Practical and Privacy-Preserving TEE Migration
    Ghada Arfaoui, Jean-François Lalande, Saïd Gharout, Jacques Traoré
    vol. 9311 9th IFIP WG 11.2 International Conference on Information Security Theory and Practice WISTP 2015 Springer LNCS 153-1682015 doi url
    Trusted execution environments (tee) are becoming widely deployed in new smartphone generation. running within the tee, the trusted applications (ta) belong to diverse service providers. each ta manipulates a profile, constituted of secret credentials and user's private data. normally, a user should be able to transfer his tee profiles from a tee to another compliant tee. however, tee profile migration implies security and privacy issues in particular for tee profiles that require explicit agreement of the service provider. in this paper, we first present our perception of the deployment and implementation of a tee: we organize the tee into security domains with different roles and privileges. based on this new model, we build a migration protocol of tee profiles ensuring its confidentiality and integrity. to this end, we use a reencryption key and an authorization token per couple of devices, per service provider and per transfer. the proposed protocol has been successfully validated by avispa, an automated security protocol validation tool.
  • Privacy and Mobile Technologies: the Need to Build a Digital Culture
    Mathilde De Saint Léger, Sébastien Gambs, Brigitte Juanals, Jean-François Lalande, Jean-Luc Minel
    Digital Intelligence DI 2014 Université de Nantes 100-1052014 url
    This paper studies the topic of privacy in its relations with mobile technologies. after presenting the complexity of the topic and the need for an interdisciplinary approach on this subject, we analyze its media coverage in the modern public space. despite the di culties high- lighted by these studies, we argue that research e orts should support the emergence of mobile services that respect users' privacy as well as the development of a digital culture of privacy.
  • A Privacy-Preserving NFC Mobile Pass for Transport Systems
    Ghada Arfaoui, Guillaume Dabosville, Sébastien Gambs, Patrick Lacharme, Jean-François Lalande
    EAI Endorsed Transactions on Mobile Communications and Applications vol. 14 5 ICST e42014 doi url
    The emergence of the nfc (near field communication) technology brings new capacities to the next generation of smartphones, but also new security and privacy challenges. indeed through its contactless interactions with external entities, the smartphone of an individual will become an essential authentication tool for service providers such as transport operators. however, from the point of view of the user, carrying a part of the service through his smartphone could be a threat for his privacy. indeed, an external attacker or the service provider himself could be tempted to track the actions of the user. in this paper, we propose a privacy-preserving contactless mobile service, in which a user's identity cannot be linked to his actions when using the transport system. the security of our proposition relies on the combination of a secure element in the smartphone and on a privacy-enhancing cryptographic protocol based on a variant of group signatures. in addition, although a user should remain anonymous and his actions unlinkable in his daily journeys, we designed a technique for lifting his anonymity in extreme circumstances. in order to guarantee the usability of our solution, we implemented a prototype demonstrating that our solution meets the major functional requirements for real transport systems: namely that the mobile pass can be validated at a gate in less than 300 ms, and this even if the battery of the smartphone is exhausted.

Control Flow Integrity for C code

september 2014

I have worked with Karine Heydemann and Pascal Berthomé on the problem of Control Flow Integrity (CFI), in the context of smart card C codes. These codes can be physically attacked during there execution for example using a laser beam. These attacks disrupts the control flow or modifies the values of the registers. Thus, the program deviates from the expected execution and may leak some secrets. We have proposed a way to harden the source code of the program in order to guarantee the integrity of the control flow. Working at source code level enables to capture several attacks with the same countermeasure. Additionally, it does not break the certification of the source code (and thus of the binary code) as our method does not require to modify the binary code of the program.

  • Software countermeasures for control flow integrity of smart card c codes
    Jean François Lalande, Karine Heydemann, Pascal Berthomé
    vol. 8713 European Symposium on Research in Computer Security ESORICS 2014 Springer International Publishing LNCS 200-2182014 doi url
    Fault attacks can target smart card programs in order to disrupt an execution and gain an advantage over the data or the embedded functionalities. among all possible attacks, control flow attacks aim at disrupting the normal execution flow. identifying harmful control flow attacks as well as designing countermeasures at software level are tedious and tricky for developers. in this paper, we propose a methodology to detect harmful intra-procedural jump attacks at source code level and to automatically inject formally-proven countermeasures. the proposed software countermeasures defeat 100\%of attacks that jump over at least two c source code statements or beyond. experiments show that the resulting code is also hardened against unexpected function calls and jump attacks at assembly level.
  • High Level Model of Control Flow Attacks for Smart Card Functional Security
    Pascal Berthome, Karine Heydemann, X. Kauffmann-Tourkestansky, Jean-Francois Lalande
    Seventh International Conference on Availability, Reliability and Security AReS 2012 IEEE Computer Society 224-2292012 doi url
    Smart card software has to implement software countermeasures to face attacks. some of these attacks are physical disruptions of chip components that cause a misbehavior in the code execution. a successful functional attack may reveal a secret or grant an undesired authorization. in this paper, we propose to model fault attacks at source level and then simulate these attacks to find out which ones are harmful. after discussing the effects of physical attacks at assembly level and going back to their consequences at source code level, the paper focuses on control flow attacks. such attacks are good candidates for the proposed model that can be used to exhaustively test the robustness of the attacked program. on the bzip2 software, the paper's results show that up to 21\%of the assembly simulated control flow attacks are covered by the c model with 30 times less test cases.
  • Attack model for verification of interval security properties for smart card C codes
    Pascal Berthomé, Karine Heydemann, Xavier Kauffmann-Tourkestansky, Jean-François Lalande
    5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security PLAS 2010 ACM 1-122010 doi url
    Smart card programs are subject to physical attacks that disturb the execution of the embedded code. these attacks enable attackers to steal valuable information or to force a malicious behavior upon the attacked code. this paper proposes a methodology to check interval security properties on smart card source codes. the goal is to identify critical attacks that violate these security properties. the verification takes place at source-level and considers all possible attacks thanks to a proposed source-level model of physical attacks. the paper defines an equivalence relation between attacks and shows that a code can be divided into areas where attacks are equivalent. thus, verifying an interval security property considering all the possible attacks requires to verify as many codes as the number of equivalence classes. this paper provides a reduction algorithm to define the classes i.e. the minimal number of attacked codes that covers all possible attacks. the paper also proposes a solution to make the property verification possible for large codes or codes having unknown source parts.

Policies and Operating System Security

june 2013

I have worked several years on mandatory access control policies for operating systems. We have proposed several models of security policies that suit different types of systems:

  • HPC Clusters where users should be isolated even if a vulnerability allows one of those to become root;
  • Emergency Systems where policies should be dynamic with the context of the crisis and the trust and reputation of the participants;
  • Large scale systems where policies can evolve and thus need to be constrained by a policy of policies.

These works have been supported by experiments using high interaction honeypots. The intruder is welcomed in a real host and is controlled by robust access control tools. It enables to capture attackers' activities. With the students of INSA Centre Val de Loire, we have developed a lightweight GUI in order to analyze the logs of different security tools installed in the honeypot (SELinux, p0f, snort, etc.). The developed software helps to better understand what is performed by attackers (see the video about Synema).

  • An extended attribute based access control model with trust and privacy: Application to a collaborative crisis management system
    Waleed W. Smari, Patrice Clemente, Jean-Francois Lalande
    Future Generation Computer Systems vol. 31 - FGCS Elsevier 147-1682014 doi url
    Many efforts in the area of computer security have been drawn to attribute-based access control (abac). compared to other adopted models, abac provides more granularity, scalability, and flexibility. this makes it a valuable access control system candidate for securing platforms and environments used for coordination and cooperation among organizations and communities, especially over open networks such as the internet. on the other hand, the basic abac model lacks provisions for context, trust and privacy issues, all of which are becoming increasingly critical, particularly in high performance distributed collaboration environments. this paper presents an extended access control model based on attributes associated with objects and subjects. it incorporates trust and privacy issues in order to make access control decisions sensitive to the cross-organizational collaboration context. several aspects of the proposed model are implemented and illustrated by a case study that shows realistic abac policies in the domain of distributed multiple organizations crisis management systems. furthermore, the paper shows a collaborative graphical tool that enables the actors in the emergency management system to make better decisions. the prototype shows how it guarantees the privacy of object's attributes, taking into account the trust of the subjects. this tool incorporates a decision engine that relies on attribute based policies and dynamic trust and privacy evaluation. the resulting platform demonstrates the integration of the abac model, the evolving context, and the attributes of actors and resources.
  • Improving Mandatory Access Control for HPC clusters
    Mathieu Blanc, Jean-François Lalande
    Future Generation Computer Systems vol. 29 3 FGCS 876-8852013 doi url
    Hpc clusters are costly resources, hence nowadays these structures tend to be co-financed by several partners. a cluster administrator has to be designated, whose duties include, amongst others, the prevention of accidental data leakage or theft. linux has been chosen as an operating system for the cea's computing platforms. however, strong system security solutions such as selinux are usually difficult to set up in large environments. this article presents how we have adapted a mac mechanism in order to enforce confidentiality and integrity between a large number of users. first we define our security objectives, and show how they direct our technical choices. then we present how confinement was achieved using the selinux security mechanism, and how various attack scenarios were addressed. we then focus on the use of mandatory categories, access control on high bandwidth network filesystems and the integration of new users and applications. we discuss some residual technical challenges. finally, we present benchmark results and validate the acceptable performance impact of our deployment on a modern cluster.
  • Security and Results of a Large-Scale High-Interaction Honeypot
    Jérémy Briffaut, Jean-François J.-F. Lalande, Christian Toinard
    Journal of Computers vol. 4 5 JCP 395-4042009 doi url
    This paper presents the design and discusses the results of a secured high-interaction honeypot. the challenge is to have a honeypot that welcomes attackers, allows userland malicious activities but prevents system corruption. the honeypot must authorize real malicious activities. it must ease the analysis of those activities. a clustered honeypot is proposed for two kinds of hosts. the first class prevents a system corruption and never has to be reinstalled. the second class assumes a system corruption but an easy reinstallation is available. various off-the-shelf security tools are deployed to detect a corruption and to ease analysis. moreover, host and network information enable a full analysis for complex scenario of attacks. the solution is totally based on open source software and has been validated over two years. a complete analysis is provided using the collected events and alarms. first, different types of malicious activities are easily reconstructed. second, correlation of alarms enables us to compare the efficiency of various off-the-shelf security tools. third, a correlation eases a complete analysis for the host and network activities. finally, complete examples of attacks are explained. ongoing works focus on recognition of complex malicious activities using a correlation grid and on distributed analysis.
  • Formalization of security properties: enforcement for MAC operating systems and verification of dynamic MAC policies
    Jérémy Briffaut, Jean-François Lalande, Christian Toinard
    International journal on advances in security vol. 2 4 325-3432009 url
    This paper focuses on the enforcement of security properties fitting with dynamic mandatory access control policies. it adds complementary results to previous works of the authors in order to better address dynamic policies. previous works of the authors provide several advances for enforcing the security of mac system. an administration language for formalizing a large set of security properties is available to system administrators. that language uses several flow operators and ease the formalization of the required security properties. a solution is also available for computing the possible violations of any security property that can be formalized using our language. that solution computes several flow graphs in order to find all the allowed activities that can violate the requested properties. that paper addresses remaining problems related to the enforcement of the same kind of properties but with dynamic mac policies. enforcement is more much complex if we consider dynamic policies since the states of those policies are theoretically infinite. a new approach is proposed for dynamic mac policies. the major idea is to use a meta-policy language for controlling the allowed evolutions of those dynamic policies. according to those meta-policy constraints, the computation problem becomes easier. the proposed solution adds meta-nodes within the considered flow graphs. a general algorithm is given for computing the required meta-nodes and the associated arcs. the proposed meta-graphs provide an overestimation of the possible flows between the different meta-nodes. the computation of the possible violations within the allowed dynamic policies is thus allowed. several concrete security properties are considered using regular expressions for identifying the requested meta- contexts. the resulting violations, within the allowed meta- graphs, are computed and real violations are presented.

About Me

Nullam turpis vestibulum et sed dolore. Nulla facilisi. Sed tortor. lobortis commodo. More ...