News
| 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. |
| Congratulations to Dr Liam O'Conner! |
|---|
| 2019-09-26 Congratulations to Liam O'Conner, who has just been awarded his PhD! Liam has been instrumental in the design of the Cogent language, a functional systems language that can be reasoned about, while producing fast C code. A major part of his thesis was formalising the refinement from a functional semantics to an imperative semantics of Cogent by using linear types. |