查看文章

New classes of concurrent programs. Concurrent programs exhibit an intractable number of possible interleavings among their concurrent sequential parts. The project allowed for defining and comparing new abstraction based model-checking techniques that could establish or refute safety properties (eg, assertion violations, runtime errors, deadlocks) for programs creating an arbitrary but finite number of concurrent threads whose correctness might depend on invariants relating values of shared variables to numbers of threads in given states, on synchronization barriers or on complex constructs such as the Habanero Java phasers [1, 2, 3, 4].

Side-channel attacks. Computer hardware makes use of complex micro-architectural constructions (eg, caches, speculative execution) to optimize program executions. New security attacks leverage such constructions to retrieve sensitive information (eg, secret crypto keys, other processes’ virtual memories). The project made possible starting a framework [5] to formally assess the vulnerability of existing mainstream software to cache-based attacks. This work has been invited to a special issue to the ACM Transactions on Embedded Computing (TECS). This line of work resulted in a Singapore-based project where the CENIIT project leader co-investigates, with Prof. Sudipta Chattopadhyay from SUTD-Singapore, a project on the “Verification and Validation of Side-channel Freedom project”. The Singapore-based project is supported by a highly competitive three-years grant from the Singapore Ministry of Education (MOE).