J. S. Shapiro, Towards a verified, general-purpose operating system kernel, Proceedings of the NICTA Formal Methods Workshop on Operating Systems Verification, 2004.

G. Ed and . Klein, NICTA Technical Report 0401005T-1. Sydney, Australia: National ICT Australia Team INDES?Secure Diffuse Programming

E. Balland and C. Consel, Open platforms, Programming Support Innovations for Emerging Distributed Applications on, PSI EtA '10, pp.1-3, 2010.
DOI : 10.1145/1940747.1940750

URL : https://hal.archives-ouvertes.fr/inria-00533721

A. Bartel, J. Klein, Y. L. Traon, and M. Monperrus, Automatically securing permission-based software by reducing the attack surface: an application to Android, Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, 2012.
DOI : 10.1145/2351676.2351722

URL : https://hal.archives-ouvertes.fr/hal-00700074

E. W. Biederman, Multiple Instances of the Global Linux Namespaces, Proceedings of the Linux Symposium, pp.101-112, 2006.

G. Daniel, L. G. Bobrow, R. P. Demichiel, S. E. Gabriel, G. Keene et al., Common Lisp Object System Specification, SIGPLAN Not. 23.SI, pp.1-142, 1988.

C. Edwin and . Brady, Idris?Systems Programming Meets Full Dependent Types, Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification. PLPV '11, 2011.

J. Bruneau and C. Consel, DiaSim: a simulator for pervasive computing applications'. In: Software: Practice and Experience 43, pp.885-909, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00715745

E. Burnette, Hello, Android: Introducing Google's Mobile Development Platform, 2009.

N. Cameron and J. Noble, Encoding Ownership Types in Java, pp.271-290, 2010.
DOI : 10.1007/978-3-642-13953-6_15

L. Caroux, C. Consel, L. Dupuy, and H. Sauzéon, Verification of daily activities of older adults, Proceedings of the 16th international ACM SIGACCESS conference on Computers & accessibility, ASSETS '14, pp.43-50, 2014.
DOI : 10.1145/2661334.2661360

URL : https://hal.archives-ouvertes.fr/hal-01015280

D. Cassou, Développement logiciel orienté paradigme de conception : la programmation dirigée par la spécification, 2011.

D. Cassou, E. Balland, C. Consel, and J. Lawall, Leveraging software architectures to guide and verify the development of sense/compute/control applications, Proceeding of the 33rd international conference on Software engineering, ICSE '11, 2011.
DOI : 10.1145/1985793.1985852

URL : https://hal.archives-ouvertes.fr/inria-00537789

D. Cassou, J. Bruneau, C. Consel, and E. Balland, Toward a Tool-Based Development Methodology for Pervasive Computing Applications, IEEE Transactions on Software Engineering, vol.38, issue.6, pp.1445-1463, 2012.
DOI : 10.1109/TSE.2011.107

A. De and C. Alves, OSGi in Depth, 2011.

H. Gregory, S. Cooper, and . Krishnamurthi, FrTime: Functional reactive programming in PLT Scheme, 2004.

A. Courtney, Frappé: Functional Reactive Programming in Java'. In: Practical Aspects of Declarative Languages Lecture Notes in Computer Science, Ramakrishnan, pp.29-44, 1990.

M. K. Dalheimer, Programming with QT: Writing portable GUI applications on Unix and Win32, 2010.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

P. Deransart, M. Jourdan, and B. Lorho, Attribute grammars: definitions, systems, and bibliography. Lecture notes in computer science, 1988.

C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen, Correct blame for contracts, ACM SIGPLAN Notices, vol.46, issue.1, pp.215-226, 2011.
DOI : 10.1145/1925844.1926410

L. Dupuy, H. Sauzéon, and C. Consel, Perceived Needs for Assistive Technologies in older adults and their caregivers'. In: womENcourage 2015, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01168399

O. Karim, D. D. Elish, B. G. Yao, X. Ryder, and . Jiang, A static assurance analysis of Android applications, 2013.

Q. Enard, Development of dependable applications: a design-driven approach, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00829477

W. Enck, Defending Users against Smartphone Apps: Techniques and Future Directions, Lecture Notes in Computer Science, vol.8, issue.5, pp.49-70, 2011.
DOI : 10.1007/978-3-642-21599-5_7

M. Fayad and D. C. Schmidt, Object-oriented application frameworks, Communications of the ACM, vol.40, issue.10, pp.32-38, 1997.
DOI : 10.1145/262793.262798

M. Feeley, SRFI 39: Parameter objects'. In: Scheme Requests for Implementation, 2003.

J. Feiler, How to Do Everything: Facebook Applications, pp.71549676-9780071549677, 2008.

M. Felleisen, R. B. Findler, and M. Flatt, Semantics Engineering with PLT Redex, pp.262062755-9780262062756, 2009.

A. Porter-felt, E. Ha, S. Egelman, A. Haney, E. Chin et al., Android permissions: User attention, comprehension, and behavior, Proceedings of the Eighth Symposium on Usable Privacy and Security, 2012.

R. Bruce-findler, J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi et al., DrScheme: a programming environment for Scheme, Journal of Functional Programming, vol.12, issue.02, pp.159-182, 2002.
DOI : 10.1017/S0956796801004208

M. Flatt, Submodules in Racket: You Want It when, Proceedings of the 12th International Conference on Generative Programming: Concepts & Experiences. GPCE '13, 2013.

M. Flatt and P. , Reference: Racket. Tech. rep. PLT-TR- 2010-1. http://racket-lang.org/tr1, 2010.

M. Fontoura, C. Braga, L. Moura, and C. Lucena, Using domain specific languages to instantiate object-oriented frameworks, IEE Proceedings?Software 147.4, pp.109-116, 2000.
DOI : 10.1049/ip-sen:20000791

M. Fowler, UML distilled: a brief guide to the standard object modeling language, 2004.

C. Fritz, S. Arzt, S. Rasthofer, E. Bodden, A. Bartel et al., Highly Precise Taint Analysis for Android Applications, 2013.

E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software, p.9780201633610, 1994.

S. Gatti, A step-wise approach for integrating QoS throughout software development process, 2014.

C. Gibler, J. Crussel, J. Erickson, and H. Chen, AndroidLeaks: Detecting Privacy Leaks in Android Applications, 2011.

J. Hallett and D. Aspinall, Towards an authorization framework for app security checking'. In: Engineering Secure Software and Systems (ESSoS) PhD Symposium. Munich, Germany. url: https://github, 2014.

N. Hardy, KeyKOS architecture, ACM SIGOPS Operating Systems Review, vol.19, issue.4, 1985.
DOI : 10.1145/858336.858337

S. Holavanalli, D. Manuel, V. Nanjundaswamy, B. Rosenberg, F. Shen et al., Flow Permissions for Android, 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp.652-657, 2013.
DOI : 10.1109/ASE.2013.6693128

R. and N. Tillmann, TouchDevelop: Programming on the Go The Expert's Voice. available at https, p.9781430261360, 2013.

K. Hyland, Dissertation Acknowledgements: The Anatomy of a Cinderella Genre'. In: Written Communication 20, pp.242-268, 2003.

B. Joy, G. Steele, J. Gosling, and G. Bracha, Java? Language Specification, 2000.

T. Kim and N. Zeldovich, Practical and Effective Sandboxing for Non-root Users, USENIX Annual Technical Conference, 2013.

E. Kohlbecker, D. P. Friedman, M. Felleisen, and B. Duba, Hygienic macro expansion, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, pp.151-161, 1986.
DOI : 10.1145/319838.319859

X. Leroy, The CompCert C verified compiler: Documentation and user's manual, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091802

M. Henry and . Levy, Capability-Based Computer Systems, p.932376223, 1984.

C. Mann and A. Starostin, A framework for static detection of privacy leaks in android applications, Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC '12, pp.1457-1462, 2012.
DOI : 10.1145/2245276.2232009

C. William and . Mann, Smart Technology for Aging, Disability, and Independence: The State of the Science, p.9780471696940, 2005.

D. Mark and J. Lamarche, Beginning iPhone Development: Exploring the iPhone SDK, Apress, 2009.
DOI : 10.1007/978-1-4842-0199-2

M. Mcshaffry and D. Graham, Game Coding Complete, p.9781133776574, 2012.

. Online, zdnet . com / hidden -android -feature - allows-users-to-fine-tune-app-permissions-7000018944

S. Mark and . Miller, Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control, 2006.

N. Mirzaei, S. Malek, C. S. , N. Esfahani, and R. Mahmood, Testing android apps through symbolic execution, ACM SIGSOFT Software Engineering Notes, vol.37, issue.6, 2012.
DOI : 10.1145/2382756.2382798

+. Mobility and . Group, App- Guarden, 2015.

G. Muller, C. Consel, R. Marlet, L. P. Barreto, F. Mérillon et al., Towards robust OSes for appliances, Proceedings of the 9th workshop on ACM SIGOPS European workshop beyond the PC: new challenges for the operating system, EW 9, pp.19-24, 2000.
DOI : 10.1145/566726.566732

URL : https://hal.archives-ouvertes.fr/inria-00072707

T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke et al., seL4: From General Purpose to a Proof of Information Flow Enforcement, 2013 IEEE Symposium on Security and Privacy, pp.415-429, 2013.
DOI : 10.1109/SP.2013.35

M. Nauman, S. Khan, and X. Zhang, Apex, Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, ASIACCS '10, pp.328-332, 2010.
DOI : 10.1145/1755688.1755732

F. Nielson, R. Hanne, C. Nielson, and . Hankin, Principles of Program Analysis, p.3540654100, 1999.
DOI : 10.1007/978-3-662-03811-6

P. Pearce, A. P. Felt, G. Nunez, and D. Wagner, AdDroid, Proceedings of the 7th ACM Symposium on Information, Computer and Communications Security, ASIACCS '12, pp.71-72, 2012.
DOI : 10.1145/2414456.2414498

B. Pierce, Types and programming languages, p.262162091, 2002.

G. Portokalidis, P. Homburg, K. Anagnostakis, and H. Bos, Paranoid Android, Proceedings of the 26th Annual Computer Security Applications Conference on, ACSAC '10, 2010.
DOI : 10.1145/1920261.1920313

A. Conference, ACSAC '10, pp.347-356, 1920261.

R. Prieto-diaz and P. Freeman, Classifying Software for Reusability, Software, IEEE 4.1, pp.6-16, 1987.
DOI : 10.1109/MS.1987.229789

D. Roberts and R. Johnson, Evolve frameworks into domain-specific languages, 3rd International Conference on Pattern Languages for Programming, 1996.

R. Rogers, J. Lombardo, Z. Mednieks, and B. Meike, Android Application Development: Programming with the Google SDK, p.9780596521479, 2009.

A. Rountev, S. Kagan, and M. Gibas, Evaluating the imprecision of static analysis, Proceedings of the ACM-SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering , PASTE '04, pp.14-16, 2004.
DOI : 10.1145/996821.996829

J. H. Saltzer and M. D. Schroeder, The protection of information in computer systems, Proceedings of the IEEE 63, 1975.
DOI : 10.1109/PROC.1975.9939

A. David and . Schmidt, Denotational Semantics: A Methodology for Language Development, pp.0-697, 1986.

M. Serrano, N. Bielova, I. Castellani, T. Rezk, and B. Serpette, Project-Team INDES?Secure Diffuse Programming, 2014.

J. S. Shapiro, M. S. Doerrie, E. Northup, S. Sridhar, and M. Miller, Towards a verified, general-purpose operating system kernel'. In: Proceedings of the NICTA Formal Methods Workshop on Operating Systems Verification, 2004.

J. S. Shapiro, J. M. Smith, and D. J. Farber, EROS: A Fast Capability System, Proceedings of the Seventeenth ACM Symposium on Operating Systems Principles. SOSP '99, pp.170-185, 1999.

J. G. Siek and W. Taha, Gradual Typing for Functional Languages, Scheme and Functional Programming Workshop, pp.81-92, 2006.

M. Snoyman, Developing Web Applications with Haskell and Yesod. O'Reilly. isbn, p.9781449316976, 2012.

R. Stevens, C. Gibler, J. Crussell, J. Erickson, and H. Chen, Investigating User Privacy in Android Ad Libraries, Mobile Security Technologies, 2012.

D. J. Sufatrio, T. Tan, . Chua, L. L. Vrizlynn, and . Thing, Securing Android, ACM Computing Surveys, vol.47, issue.4, pp.1-58, 2015.
DOI : 10.1145/2733306

S. D. Swierstra, P. R. Azero-alcocer, and J. Saraiva, Designing and Implementing Combinator Languages, José N. Oliveira and Pedro R. Henriques. Lecture Notes in Computer Science, vol.1608, pp.150-206, 1999.
DOI : 10.1007/10704973_4

R. N. Taylor, N. Medvidovic, and E. M. Dashofy, Software architecture, Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering on European software engineering conference and foundations of software engineering symposium, ESEC/FSE '09, 2009.
DOI : 10.1145/1595696.1595754

URL : https://hal.archives-ouvertes.fr/hal-00444077

S. Tobin-hochstadt, V. St-amour, R. Culpepper, M. Flatt, and M. Felleisen, Languages as libraries, ACM SIGPLAN Notices, vol.46, issue.6, pp.132-141, 2011.
DOI : 10.1145/1993316.1993514

S. Tobin-hochstadt and M. Flatt, Advanced macrology and the implementation of Typed Scheme, Proc. 8th Workshop on Scheme and Functional Programming, pp.1-14, 2007.

T. Vidas, D. Votipka, and N. Christin, All Your Droid Are Belong to Us: A Survey of Current Android Attacks, Proceedings of the 5th USENIX Conference on Offensive Technologies. WOOT'11, 2011.

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, Model checking programs, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.203-232, 2003.
DOI : 10.1109/ASE.2000.873645

N. M. Robert, J. Watson, B. Anderson, K. Laurie, and . Kennaway, Capsicum: Practical Capabilities for UNIX, 2010.

X. Wei and L. Gomez, Iulian Neamtiu and Michalis Faloutsos (2012). 'Permission Evolution in the Android Ecosystem

C. Xiao, Novel malware XcodeGhost modifies Xcode, infects Apple iOS apps and hits App Store, Online. Accessed, vol.29, issue.9, p.113, 2015.

X. Xiao and N. Tillmann, User-aware privacy control via extended static-information-flow analysis, Automated Software Engineering, vol.21, issue.4, pp.80-89, 2012.
DOI : 10.1007/s10515-014-0166-y

S. Asim, A. H. Yuksel, M. A. Zaim, and . Aydin, A Comprehensive Analysis of Android Security and Proposed Solutions, International Journal of Computer Network and Information Security, vol.12, 2014.