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.

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

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

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

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

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

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

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

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

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

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

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

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