Project | 01
Coding Safe and Secure Communication for the Internet of Things (IoT):
Proposal ready for submission.
Dr. Tzu-Chun Chen and Prof. Patrick Eugster
This project aims to assist programmers to code safe and secure communication on IoT platforms by establishing formal foundations and type disciplines to verify the correctness of communication among the IoT entities by formally proving safety and security properties. With the experiences of formalizing behavior of interactions in distributed systems in the behavioral-type approach, we aim to formalize re-configurable communication, whose scenario may modify due to the change of global/local functions/states/resources/policies, in IoT with assertions to control (i.e., permit or forbid) the interactions in communication.
Project | 02
Lightweight Verification of Software (LiveSoft)
ERC Funding LiVeSoft. 2014 - 2020
Principal applicant: Prof. Patrick Eugster
LiveSoft investigates static techniques to verify a subset of relevant and failure-prone aspects of distributed software --- interaction between components --- in a way which is lightweight and can be integrated with compilation. Our techniques will be able to sieve out many important defects upfront by pushing software reliability into the software design process. To that end LiveSoft proposes protocol types which leverage experiences with session types yet focus on fault-tolerant distributed systems by emphasizing asynchrony, failure handling and recovery, protocol composition, security, and parameterization. A main challenge is to support different system and failure models including emerging hardware trends such as hardware transactional memory and non-volatile memory rather than hardwiring speicific notions of (a)synchrony and failures.