セキュアシステムの形式検証に関する博士研究員募集

[Taro Sekiyama]

皆様

国立情報学研究所の関山です。

今年度発足した K-Program 採択課題
「ハードウェア・ソフトウェア・理論の連携によるユニバーサルTEEアーキテクチャの実現」において、プログラミング言語・形式検証の研究を行う博士研究員を募集しています。

本メールの最後に募集要項のサマリを付けている他、詳細を

  https://hackmd.io/@TaroSekiyama/H1ewltLsxx

に記載していますので、ご興味が有る方はご検討いただければと思います。

また、適任の方をご存知でしたら本メールをご転送いただけますと幸いです。

どうぞよろしくお願いいたします。

--

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.

We'd be grateful if you could spread the word to interested candidates.

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.

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, or for systems programming, like C and Rust)
- Program logics (e.g., Separation Logic)
- Formal security verification
- Program refinement
- Program verifiers based on these techniques

Experience in modeling or verifying low-level languages (such as C, Rust, assembly languages, Verilog), systems software, or hardware will also be highly valued.

Please refer to the following webpage for the scope, details, and how to apply.
  https://hackmd.io/@TaroSekiyama/H1ewltLsxx

--

関山 太朗
国立情報学研究所