]. A. Bibliographie1, R. Aaaaaaa, A. Aaaaaa, J. Bbbbbbb, V. V. Lllllll et al., GroddDroid : a gorilla for triggering malicious behaviors, International Conference on Malicious and Unwanted Software, pp.119-127, 2015.

A. Radoniaina, V. Viet-triem, T. Thomas, and S. , Information Flow Policies vs Malware, pp.22-77

B. Arnd, BKL : That's all, folks [LWN.net]. E-mail publié sur la liste de développement du noyau Linux, PATCH, vol.2020, 2011.

B. Dirk, A. J. Ccccc, T. A. Hhhhhhhhh, J. Ranjit, and M. Rupak, Sous la dir, The Blast Query Language for Software Veriication ». In : International Static Analysis Symposium, pp.2-18978, 2004.

B. Dirk, K. Alexander, . Ppppppp, . Linux-driver, and . Veriication, Sous la dir, International Symposium On Leveraging Applications of Formal Methods, Veriication and Validation, 2012.

P. Daniel, . Bb, and C. Marco, Understanding the Linux Kernel. 3 e éd. O'Reilly Media, pp.35-55

B. Neil, Sparse : a look under the hood. Linux Weekly News. 8 juin 2016. : https://lwn, p.29, 2017.

T. Y. Cccc, H. Lllll, I. K. Mmm, . Adaptive-random, and . Testing, Sous la dir, Advances in Computer Science -ASIAN 2004. Higher-Level Decision Making. Asian Computing Science Conference, pp.320-329, 2004.

C. Kees, gcc-plugins : Add initial x86_64 kernexec plugin. E-mail publié sur la liste de développement du noyau Linux. 13 jan, 2017.

C. Kees, gcc-plugins : Add structleak for more stack initialization. E-mail publié sur la liste de développement du noyau Linux. 13 jan, 2017.

C. Jonathan, Kernel building with GCC plugins. Linux Weekly News. 14 juin 2014. : https : / / lwn, p.30, 2017.

C. Jonathan, E. Jake, S. Rebecca, and . Lwn, net News from the source. Linux Weekly News, p.35, 1998.

C. Maximiliano, P. Enrique, and M. , « Runtime enforcement of noninterference by duplicating processes and their memories, p.11, 2009.

C. Maximiliano, P. Enrique, and M. Flowx, Implementación de no interferencia en Linux, pp.186-199, 2009.

C. Ron, F. Jeanne, B. K. Rrrrr, M. N. Wwwwww, F. Kenneth et al., « EEciently Computing Static Single Assignment Form and the Control Dependence Graph, In : ACM Transactions on Programming Languages and Systems, vol.13, issue.4, pp.451-490, 1991.

D. Al, CLOC ? Count Lines of Code

E. Dorothy and . Ddddddd, A Lattice Model of Secure Information Flow, Communications of the ACM, vol.195, pp.236-243, 1976.

D. Elizabeth-robling, D. Peter, and J. Ddddddd, « Certiication of programs for secure information ow Sous la dir, Communications of the ACM, vol.207, pp.504-513, 1977.

D. David, Coverage-guided kernel fuzzing with syzkaller. Linux Weekly News. 2 mar. 2016. : https://lwn, p.31, 2017.

D. Bruno and M. Leonardo-de, The Yices SMT solver. SRI International, p.123, 2006.

E. Jake, A pair of GCC plugins. Linux Weekly News. 27 jan. 2017. : https://lwn.net/Articles, p.30, 2017.

E. Jake, The kernel address sanitizer. Linux Weekly News. 14 sept. 2014. : https://lwn.net/Articles, pp.612153-612185, 2017.

E. Antony and J. Trent, « Maintaining the correctness of the Linux security modules framework, Ottawa Linux Symposium, pp.223-256, 2002.

J. Eeeeee, E. R. Ggggggg, E. K. , S. C. Nnnnn, and G. W. , « Graphviz and Dynagraph ? Static and Dynamic Graph Drawing Tools, Graph Drawing Software. Sous la dir. de M, pp.127-148, 2004.

E. William, G. Peter, C. Byung-gon, L. P. Cc, J. Jaeyeon et al., An Information- Flow Tracking System for Realtime Privacy Monitoring on Smartphones, USENIX Conference on Operating Systems Design and Implementation, pp.1-6, 2010.

J. Scott and F. , « Type qualiiers : lightweight speciications to improve software quality, Thèse de doct, p.29, 2002.

G. Tal, . Traps, and . Pitfalls, Practical Problems in System Call Interposition Based Security Tools. » In : Network and Distributed Systems Security Symposium, pp.163-176, 2003.

G. Samir and S. Fausto, Information Flow Analysis for Java Bytecode Sous la dir. de Radhia CCCCC. T. 3385, International Conference on Veriication, Model Checking, and Abstract Interpretation, pp.346-362978, 2005.

G. Laurent, V. Valérie, . Ttttt-t, M. Ludovic, K. Tools et al., A Policy-Based Intrusion Detection System Automatically Set by the Security Policy, International Workshop on Recent Advances in Intrusion Detection, pp.355-356, 2009.

G. Laurent, J. Mathieu, P. Guillaume, T. Frédéric, V. Viet-triem et al., Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory ». In : Software Engineering and Formal Methods Software Engineering & Formal Methods (SEFM 2017) Sous la dir, Lecture Notes in Computer Science, pp.1-16, 2017.

G. Laurent, J. Mathieu, P. Guillaume, T. Frédéric, V. Valérie et al., Suivi de ux d'information correct sous Linux, Approches Formelles dans l'Assistance au Développement de Logiciels, 2017.

G. Laurent, J. Mathieu, P. Guillaume, T. Frédéric, V. Valérie et al., Verifying the Reliability of Operating System- Level Information Flow Control Systems in Linux, FME Workshop on Formal Methods in Software Engineering Buenos Aires, pp.10-16, 2017.

G. Laurent, T. Frédéric, V. Valérie, . T. Ttttt, and . Kayrebt, An Activity Diagram Extraction and Visualization Toolset Designed for the Linux Codebase, IEEE Working Conference on Software Visualization, 2015.

H. «. Christophe, Détection d'intrusion dans les systèmes distribués par propagation de teinte au niveau noyau ». Doctoral thesis University of Rennes 1, juin 2013 (cf, pp.75-82

H. Christophe, B. Guillaume, and . Kblare, Logiciel. : https: //git.blare-ids.org (visité le 10, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00578853

H. «. Guillaume, Détection d'intrusions paramétrée par la politique de sécurité grâce au contrôle collaboratif des ux d'informations au sein du système d'exploitation et des applications : mise en oeuvre sous Linux pour les programmes Java, Thèse de doct, pp.11-77, 2008.

D. Richard, H. Dan, K. Joe, and M. Sqlite, Version 3.18.0, publiée le 30 mar. 2017. Logiciel. : https://www.sqlite.org, p.5, 2017.

J. Trent, E. Antony, and Z. Xiaolan, « Consistency analysis of authorization hook placement in the Linux security modules framework

J. Sushil, R. S. Ssssss, T. Barbara, D. Bbb-de-marshall, . Aaaaaa et al., Information Security : An integrated Collection of Essays. Sous la dir, Solutions to the Polyinstanciation Problem, pp.493-530, 1995.

J. «. Mathieu, Semantic Comparison of Security Policies : From Access Control Policies to Flow Properties, IEEE Symposium on Security and Privacy Workshops, pp.60-67, 2012.

J. Mathieu, A. Radoniaina, V. Valérie, . Ttttt-t, and M. Ludovic, « Secure states versus Secure executions : From access control to ow control, International Conference on Information Systems Security, pp.148-162, 2013.

J. Mathieu, V. Valérie, . Ttttt-t, and M. Ludovic, « Flow based interpretation of access control : Detection of illegal information ows T. 7093, International Conference on Information Systems Security, pp.72-86, 2011.

J. Rob, W. David, and . User, Kernel Pointer Bugs with Type Inference, USENIX Security Symposium, p.29, 2004.

J. Dave and . Trinity, Version v1.7, publiée le 28 oct. 2016. Logiciel. : https: //github.com/kernelslacker/trinity, p.2, 2017.

K. Michael and . Lca, The Trinity fuzz tester. Linux Weekly News. 6 fév. 2013. : https://lwn, p.31, 2017.

K. Alexey, M. Vadim, P. Alexander, and Z. Vladimir, « Establishing Linux Driver Veriication Process, Perspectives of Systems Informatics. International Andrei Ershov Memorial Conference on Perspectives of System Informatics. T. 5947. Lecture Notes in Computer Science

J. Leonard, D. Llp, and B. Elliott, Secure Computer Systems : A Mathematical Model MTR-2547 (ESD-TR-73-278-II), Bedford : MITRE Corp, vol.2, p.6, 1973.

C. Donald and . Ll, Trusted Computer System Evaluation Criteria (Orange Book). 5200.28-STD, pp.116-130, 1985.

L. Robert, Linux Kernel Development. 3 e éd Upper Saddle River, NJ

T. F. Llll, D. E. Ddddddd, R. R. Ssssss, M. Hhhhhhh, and W. R. Ssssssss, « The SeaView security model, IEEE Transactions on Software Engineering, vol.166, pp.593-607, 1990.

M. Douglas, M. , and J. A. Rrrrr, « Multilevel Security in the UNIX Tradition » In : Software : Practice and Experience 22, pp.673-694, 1992.

M. Mmmmmmmm and N. Nnnnn, « Fuzzing Wi-Fi Drivers to Locate Security Vulnerabilities, European Dependable Computing Conference, 2008.

M. «. Jason and G. Generic, A new tree representation for entire functions, GCC Developers Summit, pp.171-180, 2003.

P. Barton, . Mmmmmm, F. Louis, and S. Bryan, « An Empirical Study of the Reliability of UNIX Utilities, Communications of the ACM, vol.3312, pp.32-44, 1990.

J. J. Mmmmmm, « Graph database applications and concepts with Neo4j, Southern Association for Information Systems Conference Proceedings. Southern Association for Information Systems Conference. T. 24 : Association for Information Systems, pp.2013-71

J. Tobias, M. Gerald, L. Blasting-linux-code-de-lubo?, B. Boudewijn, H. Martin et al., Sous la dir, Formal Methods for Industrial Critical Systems Lecture Notes in Computer Science, vol.4346, pp.211-226978, 2006.

M. Toby, M. Daniel, B. Matthew, G. Peter, B. Timothy et al., « seL4 : From General Purpose to a Proof of Information Flow Enforcement, IEEE Symposium on Security and Privacy, pp.415-429, 2013.

M. Divya, J. Trent, G. Vinod, and . Leveraging, choice" to automate authorization hook placement, p.6, 2012.

C. M. Andrew and . Jflow, Practical Mostly-static Information Flow Control, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.228-241, 1999.

C. Andrew, . Mmmmm, and L. «. Barbara, Decentralized Model for Information Flow Control Saint-Malo, ACM Symposium on Operating Systems Principles, pp.129-142, 1997.

C. Andrew, . Mmmmm, and L. Barbara, Protecting Privacy Using the Decentralized Label Model, In : ACM Transactions on Software Engineering Methodology, vol.9, issue.17, pp.410-442, 2000.

O. Amon, L. Rsbac, and . Rsbac, Extending Linux Security Beyond the Limits, p.73, 2006.

P. Yoann, J. L. Ll, R. Rydhof, H. Gilles, and M. , « Documenting and Automating Collateral Evolutions in Linux Device Drivers, European Conference on Computer Systems, pp.247-260, 2008.

P. Hendrik, S. Carsten, and K. Wolfgang, « Towards automatic software model checking of thousands of Linux modules?a case study with Avinux, Software Testing, pp.155-172, 2009.

P. François and S. Vincent, « Information Flow Inference for ML », In : ACM Transactions on Programming Languages and Systems (TOPLAS), vol.251, pp.117-158, 2003.

H. Gordon and R. , Classes of Recursively Enumerable Sets and Their Decision Problems, Transactions of the American Mathematical Society, vol.742, pp.358-366, 1953.

R. Indrajit and D. P. Laminar, Version v2, publiée le 20 août 2014. Logiciel. : https : / / sourceforge, p.2, 2017.

R. Indrajit, D. E. , M. D. Bbbb, K. S. Mmkkkkkk, and E. W. Laminar, Practical Fine-grained Decentralized Information Flow Control, ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.63-74, 2009.

P. Rusty and R. «. , Unreliable guide to hacking the Linux kernel, p.30, 2000.

R. Andrey, UBSan : run-time undeened behavior sanity checker. E-mail publié sur la liste de développement du noyau Linux. 20 oct, 2014.

R. L. Ssss, B. D. Ff, and P. Tom, Learning Perl. 6 e éd. O'Reilly Media, juin 2011, pp.978-979

P. E. Sssss, V. S. Mmmmmmm, and M. U. Mmmmmmmmm, « Experience of improving the blast static veriication tool », In : Programming and Computer Software, vol.383, pp.134-142

K. Y. Sss, F. K. , and R. Mmmmmm, « Fuzzing the Out-of-memory Killer on Embedded Linux : An Adaptive Random Approach, In : ACM Symposium on Applied Computing, pp.387-392, 2011.

S. «. Ji?í, Automatic Bug--nding Techniques for Large Software Projects ». Doctoral thesis, pp.4-2014

S. Stephen, Add missing LSM hooks in mq_timed{send,receive} and splice, Email on the Linux Security Modules development mailing list. Email publié sur la liste de développement du noyau Linux, Juil, issue.2, 2016.

S. Stephen, C. V. Wayne, and S. , Implementing SELinux as a Linux security module. 01-043, pp.139-73, 2001.

S. «. Brad and . Sstic, Keynote -grsecurity ». Symposium sur la sécurité des technologies de l'information et des communications, pp.1-2006, 2016.

S. Brad, Why doesn't grsecurity use LSM ? grsecurity, 2008.

R. Matthew, S. , and G. , Plugins - GNU Compiler Collection (GCC) Internals. 2015. : https : / / gcc . gnu . org/onlinedocs/gccint/Plugins.html#Plugins (visité le 18, p.61, 2015.

R. Matthew, S. , and G. , Using the GNU Compiler Collection (GCC). 2013 (cf, pp.30-61

S. Erich, D. Jack, S. Horst, and M. Martin, Operating system Family / Linux. TOP500 Supercomputer Sites, top500.org/statistics, 2016.

T. Ccccccccc-x3j11, American National Standard for Information Systems ? Programming Language C. X3.159-1989, American National Standard Institute, 1989.

T. Ccc and D. Tttt, The Coq Proof Assistant Reference Manual. 14 déc. 2016 (cf, p.88

T. «. Craig, The Kernel of the Argument, p.36, 2015.

L. T. Re, Media commit causes user space to misbahave (was : Re : Linux 3.8-rc1) E-mail publié sur la liste de développement du noyau Linux. 23 déc. 2012. : https://lkml.org/lkml, p.7502, 2012.

L. T. Sparse, context" checking.. E-mail publié sur la liste de développement du noyau Linux. 30 oct, 2004.

T. Linus, The Linux Kernel Version 4.7, publiée le 24 juil. 2016. Logiciel . Linux Kernel Organization, Inc. : https://kernel.org, p.2, 2017.

T. Linus, T. Josh, and L. Christopher, Sparse ? a semantic parser for C. 2003. Logiciel. : https://sparse

V. Neil, M. J. Bbbbbbb, C. Jonathan, R. Ram, O. Guilherme et al., An Architectural Framework for User-Centric Information-Flow Security, International Symposium on Microarchitecture, pp.243-254, 2004.

V. Valérie, . Ttttt-t, C. Andrew, and M. Ludovic, « Specifying and Enforcing a Fined-Grained Information Flow Policy : Model and Experiments, p.20

W. Clark and . Security, Controls in the ADEPT-50 Time-sharing System ». In : Fall Joint Computer Conference (AFIPS 1969), pp.5-7

W. Thomas, B. Nicolas, K. Daniel, and W. Georg, « Model Checking Concurrent Linux Device Drivers, IEEE/ACM International Conference on Automated Software Engineering, 2007.

L. Kwong, Y. Heng, and Y. Droidscope, Seamlessly Reconstructing the OS and Dalvik Semantic Views for Dynamic Android Malware Analysis, USENIX Security Symposium (USENIX 2012, pp.29-29, 2012.

Y. Junfeng, K. Ted, X. Yichen, and E. Dawson, « MECA : an extensible, expressive system and language for statically checking security properties, ACM conference on Computer and Communications Security, pp.321-334, 2003.

Y. Heng, S. Dawn, E. Manuel, K. Christopher, K. Engin et al., Capturing System-wide Information Flow for Malware Detection and Analysis, ACM Conference on Computer and Communications Security, pp.116-127, 2007.

Z. Nickolai, K. Hari, D. Michael, and K. Christos, « Hardware Enforcement of Application Security Policies Using Tagged Memory, USENIX Conference on Operating Systems Design and Implementation (OSDI, pp.225-240, 2008.

Z. Xiaolan, E. Antony, and J. Trent, « Using CQUAL for Static Analysis of Authorization Hook Placement, USENIX Security Symposium : USENIX Association, pp.33-48, 2002.

Z. «. Jacob, Détection d'intrusions paramétrée par la politique par contrôle de ux de références, Thèse de doct, pp.16-2003

Z. Jacob, M. Ludovic, and B. Christophe, « An Improved Reference Flow Control Model for Policy-Based Intrusion Detection, Proceedings of the 8th European Symposium on Research in Computer Security (ESORICS, p.20, 2003.

Z. Jacob, M. Ludovic, and B. Christophe, « Experimenting with a Policy-Based HIDS Based on an Information Flow Control Model, Proceedings of the Annual Computer Security Applications Conference (ACSAC)

G. Laurent, J. Mathieu, P. Guillaume, T. Frédéric, V. Viet-triem et al., Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory ». In : Software Engineering and Formal Methods, Publications de l'auteur associées aux contributions de cette thèse Conférences internationales avec actes, pp.1-16, 2017.

C. Laurent, G. Mathieu, J. Guillaume, P. Frédéric, T. Valérie et al., Suivi de ux d'information correct sous Linux Sous la dir. d'Akram II et Nikolai K, p.54, 2017.

.. Fonctionnement-de-la-sémantique-concrète, une transition comprend un noeud plus un arc, p.98

.. Et-testcommserver, Extrait des traces émises par Weir durant l'exécution réussie de l'attaque utilisant TestCommClient, p.131