2014-08-25 Seminar Dr Han on Next-Generation Storage and Its Software

Recently, storage devices have been greatly improved in terms of both bandwidth and latency by using non-volatile memories such as Flash and PRAM. However, traditional storage software stack such as operating systems and database systems becomes major performance bottleneck since they are optimized for hard disk drives and they are not suitable for new storage devices. We call this phenomenon "slow software on fast storage". For the seminar, histories of storage devices will be given in terms of interconnection and bandwidth. Then, I will show an example of software optimizations for fast storage devices, and describe our current work about virtual memory of operating systems. Finally, I'll present our future work about application-level optimizations for fast storage devices.

2014-08-23 Doctorate Awarded
David Cock has received his Doctorate. He worked to extend seL4's assurance case to non-functional security properties. Established an empirical approach to detecting and mitigating covert and side channels.

2014-08-13 Seminar Roy on A CSP-theoretic framework of checking conformance of business processes

In this talk, we tackle the problem of conformance checking which > verifies if the event logs (observed) match/fit the reference (arbitrary) process. We use concepts from Communicating Sequential Processes (CSP), which facilitates automated analysis using PAT toolkit. By this technique one can identify all the logs which cannot be properly replayed on the process. We illustrate our approach with an example. Finally, we introduce some metrics based on conformance checking. They are related to fitness, closeness, and appropriateness of the event logs vis-a-vis reference process models. We further indicate that such a framework can be used to tackle the problem of both static and run-time compliance checking for business processes. Our work is motivated by user friendly need of employing easy input technique of models and keeping the model checking work at the back-end.

2014-08-05: Podcast Interview with Len Bass
Architect Len Bass and author of Software Architecture in Practice has been interviewed for a podcast .

2014-07-29: seL4 is open source!
Today seL4 was released as open-source. In addition to kernel and proofs, sample projects, the CAmkES component framework, and a test suite were made available. Details on how to download are at http://sel4.systems/.