Hiroyuki Katsura (桂 宏行)
I’m currently a Research Associate at University of Cambridge, working with Prof. Peter Sewell in the REMS group. I completed my PhD at the University of Tokyo under the supervision of Prof. Naoki Kobayashi, where I focused on logic-based automated verification for higher-order programs. My primary research interests lie in program analyses to improve software reliability, including automated program verification (in particular, fixpoint logic solvers), type theory, and software security techniques such as fuzzing.
Contacts
- Email:
- University:
[email protected] - Gmail:
[email protected]
- University:
- ORCID: 0000-0003-3420-4207
- Google Scholar
- GitHub: moratorium08
- Linkedin: in/hiroyuki-katsura
- Bluesky (ja): moratorium.bsky.social
Publications
- Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, Peter Sewell. Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows. PLDI 2026 (To appear).
- Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. SAS 2025. [preprint]
- Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. APLAS 2024.
- Hiroyuki Katsura, Naoki Kobayashi, and Ryosuke Sato. Higher-Order Property-Directed Reachability. ICFP 2023. [video]
- Yuki Koike, Hiroyuki Katsura, Hiromu Yakura, and Yuma Kurogome: SLOPT: Bandit Optimization Framework for Mutation-Based Fuzzing, ACSAC 2022.
- Kazuyuki Asada, Hiroyuki Katsura, and Naoki Kobayashi. On Higher-Order Reachability Games Vs May Reachability. RP 2022.
- Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, and Takeshi Tsukada. A New Refinement Type System for Automated νHFLZ Validity Checking. APLAS 2020.
Education
- Apr 2022 - Mar 2025: Doctor of Information Science Kobayashi Lab, Dept. of Computer Science, Grad School of IST, UTokyo
- Apr 2020 - Mar 2022: Master of Information Science Kobayashi Lab, Dept. of Computer Science, Grad School of IST, UTokyo
- Apr 2016 - Mar 2020: Bachelor of Science, Dept. of Information Science, School of Science, UTokyo
Experience and Activities
Grants
- JSPS (学振) Research Fellowship for Young Scientists DC2, Apr 2023 - Mar 2025 高階プログラム自動検証のさらなる発展と自動テストへの融合 (Developing Automated Higher-order Program Verification and Combination with Automated Testing): project detail(ja)
Teaching Assistants
I have been a teaching assistant three times at Dept. of Information Science, School of Science, The University of Tokyo.
- Sep 2022 - Feb 2023: Processor and Compiler Lab
- Apr 2023 - Aug 2023: Functional and Logic Programming Lab
- Sep 2020 - Feb 2021: Processor and Compiler Lab
CTF (Capture The Flag; Software Security Competition)
I have been playing CTFs as a member of a university team TSG. I also join larger teams when competing in larger contests like DEFCON. I mainly play pwnable (binary exploit) and reversing.
Here are some of my achievements in CTF contests. Note that due to the collaborative nature of CTFs, my individual contribution varied from one CTF to another :)
- AlpacaHack ID: mora
- A platform for solo CTF contests
- As a member of TSG
- SECCON 2022: International Finalists
- CTFZone 2020: Finalists
- TokyoWesterns CTF 2020: 9th
- Codeblue CTF 2018: Finalists
- SECCON 2018 International Finals: Winner
- As a member of other teams
- SECCON CTF 13 Domestic Finals: winner as a member of
BunkyoWesterns - DEFCON CTF 2024 Qualifier 11th as a member of
undef1ned - SECCON CTF Domestic Finals 2023: winner as a member of
:) - DEFCON CTF 2023: finalists as a member of
undef1ned - DEFCON CTF 2022: finalists as a member of
./V /home/r/.bin/tw - Google CTF 2020(hackceler8): finalists as a member of
I use bing
- SECCON CTF 13 Domestic Finals: winner as a member of
My CTF Challenges
I have created many CTF challenges, ranging from easy to difficult, for contests including SECCON CTF, International Cybersecurity Challenge (ICC), and TSG CTF.
My favorite ones are
- chat (pwnable) TSG CTF 2021
- Catastrophe (pwnable) TSG CTF 2021
- seccon tree (pwnable) SECCON CTF 2021
Random collection of my writeups of my challenges:
- Verified C @ ICC 2025
- SQLite of Hand @ TSG CTF 2024, co-authored with mikit
- H* @ TSG CTF 2024
- Cached File Viewer @ TSG CTF 2024, co-authored with azaika
- Warmup SQLite @ TSG CTF 2024, co-authored with mikit
- bypy @ TSG CTF 2023
- sloader @TSG CTF 2023
- 👻 @TSG CTF 2023
- Conduit @TSG CTF 2023
- seccon_tree @SECCON CTF 2021
- dis-me @SECCON CTF 2021
- cHeap @TSG CTF 2021
- Catastrophe @TSG CTF 2021
- chat @TSG CTF 2021, co-authored with azaika
- Cling @TSG CTF 2021
- Coffee @TSG CTF 2021
- Yet Another PySandbox @SECCON CTF 2020
- Yet^2 Another PySandbox @SECCON CTF 2020
- mlml@SECCON CTF 2020
- Fixer@SECCON CTF 2020
Other Activities
Internships
- Feb 2021 - Aug 2022: Ricerca Security, Tokyo
- Studied fuzzing with reinforcement learning
- Aug - Sep 2020: LINE corp, Tokyo
- Developed an automated update for hypervisors on OpenStack using Kubernetes Operator Pattern (blog post[ja]).
- Aug 2017 - Jul 2018: Flatt Inc, Tokyo
- Developed a backend infrastructure for a live commerce app
- Designed a scalable live streaming infrastructure using GCP
- Sep 2016 - Oct 2017: Unipro Inc, Tokyo
- Researched translation systems from natural language to “datastore representation” for knowledge.
Projects
- Google Summer of Code, Libvirt organization as a Participant Mar - Aug 2019
- Developed Rust bindings for libguestfs, which provides a set of tools for manipulating and communicating with virtual machine disk images (archive).
- osmium: an operating system written in Rust which runs on RISC-V
- Developed an operating system on RISC-V from scratch using Rust (article(ja), translated one by cb372).
- Repo: https://github.com/moratorium08/osmium (Stars 200+)
ISUCON
ISUCON is a Japanese contest held by LINE corp, where participants aim to fine-tune a given web service within set regulations. I have played ISUCON six times as a member of FetchDecodeExecWrite.
- ISUCON 14 20th
- ISUCON 13 5th
- ISUCON 12 5th
- ISUCON 11 3rd
- ISUCON 10 6th
- ISUCON 9 finalists
- ISUCON 8 finalists
Security Camp
Hobbies
Apart from researching, I’m a big fan of
- Capture The Flag (security competition), especially pwnable
- Low-level programming
- Brewing drip coffee “nicely”
- Bouldering / Climbing
- Board games