[Haskell] Postdoc positions on Formal Verification for Zero-Trust IoT Systems at Kyoto University and National Institute of Informatics (NII), Japan

[Taro Sekiyama]

[Please distribute, apologies for multiple postings.]

Dear All,

We are seeking a few postdoc researchers, who works for a project 
“Zero-Trust IoT Systems by Collaboration of Formal Verification and 
System Software” by Japan Science and Technology Agency.

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


* Project Description

The project aims at the construction of formally verified secure IoT 
systems that follow the concept of “zero trust architecture”, dubbed 
ZT-IoT systems. It consists of four research teams and two teams, led by 
Atsushi Igarashi, Kyoto University, Japan and Taro Sekiyama, National 
Institute of Informatics, Japan (NII) are investigating applications of 
formal verification or programming language techniques to the 
construction of secure IoT systems.

The main research topic of Igarashi’s team is centered around the design 
and theory of security policy engines for ZT-IoT systems, inclucing the 
design of a language to describe security policies and policy 
enforcement algorithms and the techniques for verifying policy 
enforcement algorithms against given security policies. Other team 
members are Kohei Suenaga and Masaki Waga at Kyoto University.

The main research topic of Sekiyama’s team is centered around techniques 
for monitoring and intervention for ZT-IoT systems. Other team members 
include Ichiro Hasuo and Shin-ya Katsumata at NII.

Although the two teams are based in different places, we collaborate 
closely with each other.

The appointment can start as early as April 2022 (the starting date is 
negotiable). The contract will initially run until the end of March 
2023, with the possibility of annual renewal until the end of the 
project, which is March 2027 at maximum. Salary will be about 
360,000–550,000 JPY/month.

Applicants should have a Ph.D in computer science or related fields, and 
have a strong background in formal verification and/or programming 
language theory. Due to the project’s nature, they are required to have 
strong interests in applying theory to practice; they should also be 
(self-)motivated, dedicated, and able to work both independently and 
collaboratively. Strong communication skills in oral and written English 
are required.


* Workplace

Members of Igarashi’s team will work at Kyoto University, Kyoto, Japan 
and members of Sekiyama’s team will work at NII, Tokyo, Japan.

(Living costs in Japan are not very high nowadays. An estimate is found here
https://www.internations.org/go/moving-to-japan/living/the-cost-of-living-in-japan#:~:text=A%20single%20person%20living%20in,will%20see%20that%20number%20tripled
and we find rent can be cheaper than the cited amount.)


* Applications and inquiries

Inquiries can be sent to application-zt-iot [at] fos.kuis.kyoto-u.ac.jp, 
with the subject CREST Job Inquiry. Feel free to ask us any questions on 
relevance, topics, compensation, etc. We will reply when we see enough 
relevance.

Applications should be made electronically via the following JREC-IN 
Portal web sites.

NII: 
https://jrecin.jst.go.jp/seek/SeekJorDetail?fn=3&ln=1&id=D122010021&ln_jor=1
Kyoto: 
https://jrecin.jst.go.jp/seek/SeekJorDetail?fn=3&ln=1&id=D121122219&ln_jor=1

Please upload a pdf including

- your brief CV,
- short description of research interests (can be very informal and short),
- the list of papers (a dblp or Google scholar link will do, for example),
- a couple of representative papers (in pdf), and
- (preferably) the contact of two references.

We will contact you for further material and interview, provided that we 
find sufficient relevance in your application. Starting dates are 
negotiable. The positions will remain open until filled.


Many thanks,
Taro.