Recruiting Postdocs: Formal Verification of TEE Architectures

# Recruiting Postdocs: Formal Verification of TEE Architectures ## TL;DR We are recruiting postdocs to work on formal methods and programming languages for the formal verification of TEE architectures at [National Institue of Informatics (NII)](https://www.nii.ac.jp/en/) / [Research Organization of Information and Systems (ROIS)](https://www.rois.ac.jp/en/index.html), Tokyo, Japan. This position is especially suited for programming language or program verification researchers seeking a new application domain at the intersection of systems programming, security, and hardware, with opportunities to develop new theory accordingly. As of Sep 2025, we have two open positions. ## Description We are seeking postdocs to join the project *“Universal TEE Architecture by Collaboration of Software, Hardware, and Theory”*, funded by the Japan Science and Technology Agency. The project aims to construct a formally verified secure TEE architecture. A TEE (Trusted Execution Environment) is a hardware-based technology that provides an execution environment isolating applications and sensitive data from untrusted underlying systems (including the OS and hypervisor); see [1][2] for more details. [1] [Introduction to Trusted Execution Environments – GlobalPlatform](https://globalplatform.org/resource-publication/introduction-to-trusted-execution-environments/) [2] [Trusted Execution Environment: What It Is, and What It Is Not – IEEE](https://ieeexplore.ieee.org/document/7345265) The project consists of three research areas: systems software, hardware, and formal verification. The formal verification team, led by [Taro Sekiyama](https://skymountain.github.io/) at [Center for Research and Development on Secure Computer Systems (CRADSEC)](https://cradsec.rois.ac.jp/) / [National Institute of Informatics (NII)](https://www.nii.ac.jp/en/) in [Research Organization of Information and Systems (ROIS)](https://www.rois.ac.jp/en/index.html), Tokyo, Japan, is responsible for formally verifying the TEE architecture designed by the software and hardware teams, using formal methods and programming language techniques. Relevant techniques (but not limited to) include: - Proof assistants (e.g., Rocq and Agda) - Type systems (especially for verification, like refinement and dependent type systems, for for systems programming, like C and Rust) - Program logics (e.g., Separation Logic) - Formal security verification - Program refinement - Program verifiers based on the these techniques Experience in modeling or verifying low-level languages (such as C, Rust, assembly languages, and Verilog), systems software, or hardware will also be highly valued. The appointment can begin as soon as possible (starting date negotiable). The initial contract runs until the end of March 2026, with the possibility of annual renewal until the end of the project (March 2030 at the latest). The monthly salary will be approximately 360,000–600,000 JPY. Applicants should hold a Ph.D. in computer science or a related field, with a strong background in formal verification and/or programming language theory. A record of publications demonstrating expertise in these areas is highly desirable. Given the nature of the project, candidates should have a strong interest in applying theory to practice. They are expected to be self-motivated, dedicated, and capable of working both independently and collaboratively. Proficiency in written and spoken English is required. ## Workplace [WeWork Jinbocho](https://wework.co.jp/en/location/tokyo/kanda-jimbocho-area/jimbocho), Tokyo, Japan. The cost of living in Japan is currently not very high. See [Numbeo](https://www.numbeo.com/cost-of-living/in/Tokyo) for estimates (housing is often available at lower rents than those listed there). ## Applications and Inquiries Inquiries may be sent to **sekiyama _at_ nii.ac.jp** with the subject line *“TEE Veirifcation Job Inquiry”*. Feel free to ask any questions regarding relevance, topics, compensation, etc. We will respond only if we find sufficient relevance. Applications should also be sent to **sekiyama _at_ nii.ac.jp** with the subject *“TEE Veirifcation Job Application”*. Please upload a single ZIP file containing: - a brief CV in PDF, - a short description of research interests (informal is fine), - a publication list (e.g., dblp or Google Scholar link), - a couple of representative papers (PDFs), and - preferably, contact information for two references. If we find sufficient relevance, we will contact you for further materials and an interview. Starting dates are negotiable. Positions remain open until filled.