ZT-IoT Research Topics
https://zt-iot.nii.ac.jp/en/Formal Verification

Monitoring & Policy Enforcement

Camera Appl.
(Libcamera,Gstreamer)

No Perfor m ance De gradation

Monitoring& Enforcement

Monitor(Auditd, Plugin)
Enforcementer(compsec)

Coordinator(MQTT Broker)

Rest APIServer(Flask)

The Higher the Better

Security
controller

Linux Kernel
The Lower the Better

Raspberry Pi 4 Model B

70 % De gradation(Coretex-A7 @1.5 GHz x 4)

Arducam PTZ Camera(Sony IMX477 CMOS)• A monitoring and enforcement framework* basedon Linux Audit and MQTT for IoT devices is being
designed and implemented.

procedure CameraServer {ServerREE :for i in range(3) {let p = recv(ch);let res = verify(p.snd, p.fst, pkey);if (res) {skip @ !ImgRecvValid(p.fst);} else {skip @ !ImgRecvInvalid(p.fst);}}}
procedure CameraClient {ClientREE :let image_fd = open(campath);copy skeypath to ClientTEE as t_skeypath;
ClientTEE :let skey0 = read_from_path(t_skeypath);
let skey = dec(skey0, fek);
ClientREE :for i in range(3) {let image = read(image_fd);
copy image to ClientTEE as t_image;
ClientTEE :let t_sig = sign(t_image, skey);
copy t_sig to ClientREE as sig;
ClientREE :send(ch, (image, sig)) @ !ImgSend(image);}}φ(1) Model asystem
by Rabbit

Lemma ⦅φ⦆(2) Translate
Rabbit toTamarin Prover

Security req.

System model M(Rabbit model)translate
Tamarin model ⦅M⦆

Tamarin ProverYes⦅M⦆ ⊧ ⦅φ⦆?

Noverified(3) Verify themodelfalsified by TamarinProver• As shown in the above figure, a prototype system
carries out a real-time execution environment for
application and system security monitoring using
optimum process-to-core mapping. Many existing
works using Linux Audit pointed out theundesirable runtime overhead to the system.

• Rabbit is a system modeling language for formallyverifying cybersecurity, its main target being nonexperts in formal verification.
• The (current) implementation of Rabbit works as atranslator to the input lang. of the Tamarin Prover**,which is a model checker for security protocols.
• Unlike Tamarin, which is based on the theory ofmultiset rewriting, Rabbit provides more familiar
syntax to describe IoT systems.

* A Linux Audit and MQTT-based Security Monitoring Framework," IEEE COMPSAC 2023, June 2023.

** Tamarin Prover: https://tamarin-prover.github.io/

Software Certification Service

Tiered Key Management using TEE

Certificate
Authority
Cert.

AR
SoftwareRepository
SW
sign

AR
sign

IoT ServiceApp. 1

IoT ServiceApp. 2

Tier-2 Certificate
w/ CA, T1 signs,
T2 Public key

IoT Device w/
Hardware Security Module(HSM)

Tier-1 Certificate
w/ CA sign,
T1 Public key

OS

sign

CI/CDComm Comm
2122

Tier-3 Certificatew/ CA, T2 signs,T3 Public key

sign

Cert: Certificate
SW: Software
AR: Assessment Results• Security in research software, or software
reliability, is now a crucial issue in researchcommunities to certify that research software isproperly and securely executed.
• We propose a software certification framework toassure software reliability, where the user canconfirm:• The integrity of the software by the digital
signature of the software developer/integrator• The vulnerability assessment results from thedigital signature of the authorized third-party
organization.

Tier-3 Secret Key
sign
Tier-2 Secret Keysign

Trust Chain

Software
AssessorSW

sign

SoftwareUser

Comm Comm
1112Cert.

SoftwareDeveloper/Integrator
SW

TEE / Secure World

REE / Normal World

Tier-1 Secret Key(stored in HSM)

Hardware Root of Trust (RoT)• We propose a tiered PKI key management
scheme using TEE to address integrity andauthenticity:• A multi-authenticator model is applied to realize
the trust chain from RoT.
• Hardware RoT is used as the Tier-1 secret key.
• Tier-2/Tier-3 keys are generated and stored in
TEE for each application/communication.
• We have developed the prototype system usingArm TrustZone, OP-TEE, and PKCS #11 andconfirmed that the secret key stored
in TEE can be used in client auth. ofthe MQTT communication over TLS.

This work was supported by JST, CREST Grant Number JPMJCR21M3.

National Institute of Informatics
https://ccrd.nii.ac.jp/sc23/