News
|
TS wins ACM SIGOPS Hall of Fame Award
|
|---|
|
2019-11-07 We have won the ACM Special Interest Group in
Operating Systems (SIGOPS) Hall of Fame Award for our
paper: seL4: Formal Verification of an OS Kernel published at the 2009 ACM SIGOPS Symposium on Operating Systems Principles (SOSP). This award recognises "the most influential Operating Systems papers that were published at least ten years in the past." The citation notes that "the work has become the basis for a large amount of subsequent work in provably correct systems.”. Congratulations! See more detail here. |
| 2019-11-05 Upcoming Seminar on DARPA Cyber Assurance Briefings |
|---|
|
Dr. Raymond Richards is the Program Manager for DARPA's Cyber Assured Systems Engineering (CASE) and Automated Rapid Certification Of Software (ARCOS) Programs. CASE is developing cutting-edge methods and tools for the creation of systems that are inherently resilient to cyber-attacks. ARCOS will apply data analytics to assurance evidence to develop arguments that software is fit for use.
On the Friday, 8th of November 2019 we invite you to
attend Dr. Raymond Richard's seminar. This seminar will
provide an:
Details:
Location: Seminar Room 113, Level 1, Building K17
UNSW
Date: Friday, 8th of November
2019
Time: 10:00am - 11:30am
|
| Announcing the seL4 Foundation |
|---|
| 2019-10-21 With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing, and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. |
| Qian Ge and co-authors win Best Paper award at EuroSys 2019 |
|---|
|
2019-10-10
The paper "Time Protection: The Missing OS Concept”
by Qian Ge, Yuval Yarom, Tom Chothia (U Birmingham) and
Gernot Heiser won Best Paper at the Tier-1 EuroSys
conference in Dresden, Germany. It presents the first
principled approach to preventing information leakage by
timing channels, a problem the research community had
ignored until it was highlighted by the Spectre exploit a
year ago. The paper defines the new concept of time
protection, shows how it can be implemented in the
high-assurance seL4 microkernel, and demonstrates that it
is highly effective in eliminating information leakage to
the degree that hardware provides the right mechanisms. The
results also confirm the team’s earlier claims that
true information security will need a
new hardware-software contract. You can see more
here. Congrats to the team! |
| Congratulations to Dr Qian Ge! |
|---|
|
2019-10-04
Congratualtions to Dr Qian Ge, who has just been
awarded her PhD! Qian had been working on inventing highly optimised OS mechanisms for mitigating microarchitectural timing channels which obtain data leakage through resource contention. Her and her co-authors proposed a new system concept, time protection, as an OS abstraction, which offers mandatory temporal isolation analogous to the spatial isolation provided by the established memory protection abstraction. Time protection provides security guarantees against microarchitectural timing channels through a combination of temporal and spatial isolation techniques. Using our prototype in the seL4 microkernel, they demonstrated that time protection is both lightweight and effective. |