Resume

Protocol engineer on the delta network (Rust).

• Documented the SDK and base libraries for early app developers.
• Modularized domain tasks; fixed transaction-application logic; typed abstractions.
• Added NFT support; designed and built the archive node.
• Built the integration-testing API and its test suite.

Crypto & protocol engineer on the Mina Protocol.

• Codebase-wide cleanup, refactoring and higher test coverage (OCaml, Nix).
• o1vm / Optimism: low-level communication with the fault-proof op-program (Rust, Go).
• Berkeley hard fork: pre/post-fork test harness.
• Prototyped account deletion (core zkApps feature); chunking.

• Led the consensus team (from July 2021).
• Implemented the Tenderbake consensus for the Ithaca protocol upgrade; maintenance.
• Test maintenance and migration Python → Tezt for the new consensus.
• Merge Team (core reviewers) member.

Project lead & consultant.

• Tezos clients (mockup/proxy client, Sapling client).
• Gerrit plugins (enforce owner approval, CI-related UI extensions).
• Built the internship program (setup, outreach, selection).

• Development of (formal) program analyses on source and binary code, for safer and more secure software engineering.
• Lead developer and team co-lead of the open-source binary-analysis and symbolic-execution platform BINSEC.
• Co-advisor and day-to-day supervisor of two PhD students, plus MSc interns (see Students).
• Lectures on software attacks & vulnerabilities (ENSTA).

Teaching (programming, formal methods); research on the constraint solvers used in software verification: veriT SMT solver, SMTpp, the Portugol online interpreter.

Generation of construction functions respecting algebraic invariants for OCaml.

Teaching assistant.

Thesis: Tableaux et déduction modulo (Tableaux and Deduction Modulo), defended 17 October 2006. Automated theorem proving, rewriting, proof theory.

Formal methods platform for security-oriented binary code analysis (symbolic execution, fuzzing, code deobfuscation, …).

C/C++ software analyzers — plugins metrics and mthread (initial version).

Preprocessing platform for SMT-LIB, the problem repository for SMT solvers.

Web application for users to play with the PathCrawler test generation tool.

Construction functions generator for datatypes with (algebraic) invariants.

Automatic verification of low-level code: C, assembly & binary code.

Advanced fuzzing techniques for vulnerability discoveries at scale.

WPTrans: assistant for program verification in Frama-C.

Combining formal and learning approaches for binary-level security analysis.

Combining fuzzing and symbolic execution for vulnerability detection.

Sharpening symbolic methods for vulnerability detection.

• J. Rosain, R. Bonichon, J. Cailler, O. Hermant. A Generic Deskolemization Strategy. LPAR 2024, EPiC Series in Computing 100, p. 246–263. doi

• T. McDonald, R. Manikyam, S. Bardin, R. Bonichon, T. R. Andel. Program Protection Through Software-Based Hardware Abstraction. SECRYPT 2021. pdf
• G. Menguy, S. Bardin, R. Bonichon, C. de Souza Lima. Search-based Approaches for Local Blackbox Deobfuscation: Understand, Improve and Mitigate. CCS 2021. pdf
• F. Recoules, S. Bardin, R. Bonichon, M. Lemerre, L. Mounier, M.-L. Potet. Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine. ICSE 2021 — Distinguished Paper Award. pdf

• M. D. Nguyen, S. Bardin, R. Bonichon, R. Groz, M. Lemerre. Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities. RAID 2020. pdf
• F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet. Et TInA RUSTInA le lien vers l'assembleur. JFLA 2020. pdf

• M. Ollivier, S. Bardin, R. Bonichon, J.-Y. Marion. How to Kill Symbolic Deobfuscation for Free (or: Unleashing the Potential of Path-Oriented Protections). ACSAC 2019. pdf
• M. Ollivier, S. Bardin, R. Bonichon, J.-Y. Marion. Obfuscation: Where Are We in Anti-DSE Protections? (a first attempt). SSPREW 2019. pdf
• F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet. Get rid of inline assembly through verification-oriented lifting. ASE 2019. pdf
• F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet. De l'assembleur sur la ligne ? Appelez TInA !. JFLA 2019. pdf
• B. Farinier, S. Bardin, R. Bonichon, M.-L. Potet. En finir avec les faux positifs grâce à l’exécution symbolique robuste. JFLA 2019. pdf

• B. Farinier, S. Bardin, R. Bonichon, M.-L. Potet. Model Generation for Quantified Formulas: A Taint-Based Approach. CAV 2018. pdf

• R. Bonichon, P. Weis. Format unraveled. JFLA 2017. pdf · slides

• R. Bonichon, O. Hermant. A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization. CoRR abs/1505.06376. arxiv
• R. Bonichon, D. Déharbe, P. Dobal, C. Tavares. SMTpp: preprocessors and analyzers for SMT-LIB. SMT Workshop 2015. pdf

• R. Bonichon, D. Déharbe, T. Lecomte, V. Medeiros Jr. LLVM-Based Code Generation for B. SBMF 2014.
• R. Bonichon, D. Déharbe, C. Tavares. Extending SMT-LIB v2 with \(\lambda\)-Terms and Polymorphism. SMT Workshop 2014. pdf

• R. Bonichon, P. Cuoq. A Mergeable Interval Map. Stud. Inform. Univ. 9(1), p. 5–37. pdf
• R. Bonichon, G. Canet, L. Correnson, E. Goubault, E. Haucourt, M. Hirschowitz, S. Labbé, S. Mimram. Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software. SAFECOMP 2011, p. 85–98. pdf · doi

• R. Bonichon, D. Delahaye, D. Doligez. Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007. pdf

• R. Bonichon, O. Hermant. On Constructive Cut Admissibility in Deduction Modulo. TYPES 2006. pdf
• R. Bonichon, O. Hermant. A semantic completeness proof for TaMeD. LPAR 2006. pdf

• R. Bonichon. TaMeD: A Tableau Method for Deduction Modulo. IJCAR 2004, p. 445–459. pdf · doi