Older Events
|
Proof that seL4 enforces confidentiality established for RISC-V
|
|---|
2021-12-02 – In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity, following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V. The next step in the assurance stack is now also completed for RISC-V with the proof that seL4 enforces confidentiality, i.e. that seL4 provably enforces information flow control, when it is correctly configured to do so. “This completes the 3 big CIA security properties for seL4 on RISC-V: confidentiality, integrity and availability. While integrity ensures there is no unauthorised interference with private data, confidentiality ensures there is no unauthorised access to private data”, says Gernot Heiser, chair of the seL4 Foundation. Special thanks to TS's Ryan Barry, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. The proof is available on GitHub. |
|
New partnership formed to protect human rights organisations from cyber-attacks
|
2021-11-29 – UNSW Sydney has signed a research agreement with Swiss technology company Neutrality to develop cyber network safeguards for organisations whose integrity and trust is essential in protecting people. “This project aims at protecting communications of humanitarian and other non-government organisations from cyber-attacks, which often result in loss of lives”, said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser. “Trustworthy Systems will work with Neutrality in the development of such secure communication, leveraging the mathematically proved security enforcement provided by our seL4 microkernel technology.” |
|
Alaska Center for Energy Power joins the Laot team
|
| 2021-10-27 – The Alaska Center for Energy and Power (ACEP) has joined the Laot project team. ACEP will conduct tests and demonstrations in their Fairbanks facility. |
|
First release of the seL4 Core Platform
|
| 2021-10-22 – The seL4 Core Platform (seL4CP) has been proposed in an seL4 RFC. It was co-designed and -implemented with the Laot project and has now been publicly released for feedback and (eventual) TSC endorsement. |
|
Gernot explains why seL4 is safe – and the role of TS
|
| 2021-09-28 – Following CSIRO's abandoning of TS and the seL4 technology TS developed, the seL4 community and the seL4 Foundation have grown a lot. This has led to concerns that the broader participation might have the potential to undermine the integrity of seL4. In his latest blog, Gernot explains why there is no reason for such concern, and how TS is re-building to continue driving the research that keeps seL4 define the state of the art. |
|
TS services receive interim endorsement from the seL4 Foundation
|
| 2021-08-22 – The seL4 Foundation has given interim endorsement to TS as a trusted provider for services around seL4. |
|
seL4 protects world's most secure drone from DEFCON hackers
|
|
2021-08-13 – On 6
August DARPA brought the
“SMACCMcopter”
to DEF CON
and invited the assembled hacker elite to attack it. The
SMACCMcopter was the research vehicle of the Air Team at
DARPA's HACMS
program. The Trustworthy Systems
team worked
with project partners to deploy seL4 and leverage formal
methods to protect the drone from cyber attacks. The result? Predictably, sel4's verified security enforcement defeated the hackers comprehensively. As DARPA said: “Formal methods FTW!” |
|
Proof that seL4 enforces integrity established for RISC-V
|
|
2021-07-28 –
The assurance story for seL4
on RISC-V keeps building. We first
formally proved functional
correctness: that
the seL4 C code on RISC-V platforms behaves exactly as its
specification says. We then established binary
correctness: that
the machine code running on the processor behaves exactly as the C
code, and by extension, as the specification says. We now have
established the crucial integrity property for
seL4 on RISC-V: that the specification, and by extension the kernel
binary, prevents an application running on top from modifying data
without authorisation. In seL4 speak: seL4 provably enforces
capability-based access control. “The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.” Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. See Gernot's blog for more details. The proof is available on GitHub. |
|
The Trustworthy Systems Group is now back at UNSW
|
|
2021-07-21 – The Trustworthy Systems (TS) grew to world fame
in NICTA,
with the design, implementation and verification
of seL4 its defining achievement. When
NICTA was absorbed
into CSIRO's Data61 in
mid-2015, TS became part of it, and was one of a small number
of groups that defined Data61's international reputation. We
attracted millions of dollars in funding every year from
government organisations such
as DARPA and industry
players such as HENSOLDT
Cyber. Despite all that, Data61 has withered TS down from over 50 people two years ago to less than twenty. In May CSIRO management finally announced that TS is no longer wanted, for reasons that are hard to fathom. We are extremely grateful to UNSW's School of Computer Science and Engineering for giving us a new home and some bridging funding that allows us to continue operate and rebuild. We will continue perform world-leading research and technology transfer on seL4 and its ecosystem, and support the seL4 community as part of the seL4 Foundation. Specifically we are keen to engage with organisations that can provide funding for our work. |
|
seL4 on RISC-V is verified to the binary
|
|
2021-05-05 – The seL4 Foundation and
RISC-V International announced that the
verified seL4 microkernel on the RV64 architecture has been proved
down to the executable code
by the Trustworthy Systems group, thanks to
funding provided by HENSOLDT
Cyber GmbH. This guarantees that the seL4 microkernel on RV64
will operate to specification even when built with an untrusted C
compiler, GCC. For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance). |
|
Gernot has been appointed as one of ACM’s
Distinguished Speakers
|
| 2021-05-04 Professor Gernot Heiser has been appointed as one of ACM's Distinguished Speakers, "Renowned International Thought Leaders Speaking on the Most Important Topics in Computing Today"!
You can see the full list of speakers here. Congratulations to Gernot for joining this illustrious group! |
|
Gernot Heiser and ETH Zurich co-authors win Best Paper award at
DATE'21
|
| The paper “Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core” by Nils Wistoff, Moritz Schneider, Frank K. Gurkaynak, Luca Benini and Gernot Heiser won Best Paper at the Tier-1 Design, Automation and Test in Europe (DATE) conference. |
|
seL4 is verified on RISC-V
|
|
2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.
We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. You can find more details about the verification of seL4 on RISC-V on Gernot's blog |
|
seL4 teaching videos available
|
|
2020-06-02 – Yet another contribution of UNSW
Sydney to the seL4 community: This year Gernot Heiser is making
the seL4-related videos from his UNSW Advanced Operating Systems
class freely available. You’ll find them at
the UNSW
CSeLearning COMP9242 YouTube channel. At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site. |
|
Announcing the seL4 Foundation whitepaper: "The seL4
Microkernel – An Introduction"
|
| 2020-05-25 This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems.
You can download it at https://sel4.systems/About/ |
|
The seL4 Foundation has launched
|
|
2020-04-07 We have taken an exciting step to expand the seL4 community, by setting up the seL4 Foundation. It forms an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It brings together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those adopting seL4 in real-world systems. Its focus is 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.
You can learn more by visiting the seL4 Foundation section of our newly revamped sel4.systems website, or reading Gernot's announcement blog. |
|
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. |
| 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. |
| 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. |
| Johannes Aman Pohjola has won best paper at FORTE and at the DisCoTeC federated conference |
|
Johannes Aman Pohjola has won best paper at FORTE 2019 and
at the DisCoTeC 2019 federated conference. The paper covers
the standard theoretical models of concurrent systems with
explicit communication channels, such as the pi-calculus,
which give rise to symmetric and transitive connectivity
between processes. That is, if I can send a message to you,
it follows that you can send a message to me, and that I
can send a message to anyone you can send to. In this
paper, this somewhat unrealistic assumption is relaxed by
developing a more general model where channels can denote
any connectivity relation, including one-way connections or
connections that change over time. Congratulations Johannes! |
| Qian Ge and co-authors win Best Paper award at EuroSys 2019 |
|
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! |
| June Andronick is an invited speaker to FM'19 |
| FM '19 is the third world congress on Formal Methods (held every 10 years). It's is in Porto this October, where our research group leader June Andronick is an invited speaker! You can learn more about FM'19 from this video. |
| seL4 in spaaace! |
| The UNSW QB50 satellite UNSW-EC0 has just burned up in the earth’s atmosphere after 18 months in space. The satellite carried an seL4-based payload that operated successfully under space conditions. |
| Professor Gernot Heiser, Dr Toby Murray, and Professor Gerwin Klein have won an ARC discovery grant for their work on provable time protection |
| 2018-11-18 Professor Gernot Heiser, Dr Toby Murray, and Professor Gerwin Klein have won an ARC discovery grant for their work on provable time protection. This project aims to develop techniques to solve the issue in information security of unauthorised information flow resulting from competition for shared hardware resources. The project will combine operating systems design, formal hardware models, information-flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. The project is expected to result in a system that prevents leakage of critical information, such as encryption keys, through timing channels. This should prevent sophisticated attacks on public clouds, mobile devices and military-grade cross-domain devices. |
| Thomas Sewell is a 2019 CORE Award Winner! |
|
CORE (Computing Research & Education) have awarded
Thomas Sewell the John Makepeace Bennett Award for the
Australasian Distinguished Doctoral Dissertation! Thomas' PhD on binary translation validation is a breakthrough in formal verification: it manages to prove that the binary code emitted by a standard gcc compiler correctly implements the semantics of the input C program. His tool chain produces a separate proof for each input program -- when gcc produces correct output, the tool confirms with a proof, and when gcc produces incorrect output, it rejects. This is highly significant, as it means that the compiler no longer has to be trusted, and an off-the-shelf low-assurance compiler can be used to produce high-assurance code. The tool chain and methods developed in Thomas' PhD have further applications beyond binary verification. In particular, it enables making an analysis for worst-case execution time (WCET) to be more precise and highly assured. |
| First Annual seL4 Summit |
|
Supported by Defense Advanced Research Projects Agency
(DARPA) and Air Force Research Laboratory (AFRL), the first
Annual seL4 Summit will be held on November 14-16, 2018 at
the Hilton Washington Dulles Airport, Herndon, VA. seL4 is the first formally verified microkernel, which offers fundamental software separation properties and provides new opportunities to build assured computer systems. The seL4 Summit is part of an effort to establish a Center of Excellence for seL4 ecosystems, aiming to mature the seL4 technology, stabilize the software distribution, train and expand the user base, and develop needed capabilities. The development of seL4 was supported by the Defense Advanced Research Projects Agency (DARPA) under the High-Assurance Cyber Military Systems (HACMS) program, which aims to create technology for the construction of high-assurance cyber-physical systems, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties. Information about Summit agenda, venue and registration can be found at https://www.sel4-us.org/summit. |
| Qian Ge and co-authors win Best Paper award at APSys 2018 |
| The paper “No security without time protection: we need a new hardware-software contract” by Qian Ge, Yuval Yarom and Gernot Heiser won Best Paper at the APSys Workshop in Korea. It demonstrates that contemporary processors lack the mechanisms that the operating system (OS) needs to prevent timing channels of the kind that enable the Spectre attacks. The paper consequently proposes an improved hardware-software contract that gives the OS the means to prevent such channels. |
| Data61's Trustworthy Systems announces global partnership with Hensoldt Cyber |
| Data61's Trustworthy Systems has announced a global partnership with German cyber security company Hensoldt Cyber to collaborate on the development of a trustworthy hardware-software stack designed to protect against devastating cyber-attacks on defence systems, smart factories, autonomous vehicles and critical infrastructure. |
| seL4 now runs on RISC-V64 |
| 2018-04-18 Release 9.0.1 of the seL4 kernel has prototype support for RISC-V64. At the time of release, seL4-test passes on the Spike emulation platform, with single core, and without FPU. Full details were released to the seL4 devel mailing list |
| Everything you’ve been told about passwords is wrong |
|
2018-02-19 The US expert who wrote the standard for
password security now says he was wrong — and it's
time for a new way. Gernot Heiser has been interviewed by InTheBlack about computer security regarding passwords — and that part of the solution is to use long, memorable passphrases rather than passwords. |
| seL4 based AltoCrypt secure communication device wins AU Army development contract |
|
2018-02-19 Australian company Penten Services has won a
$1.3m innovation contract for their seL4 based AltoCrypt
secure communication device. The device will provide secure
wireless communication to the army to protect it from cyber
threats. Read more here. |
| Gernot Heiser joined editorial board of the Research Highlights section of Comm. of the ACM |
| 2018-02-12 Gernot Heiser has joined the editorial board of the highly prestigious Research Highlights section of Communications of the ACM. 24 Research Highlights are invited per year from the most impactful work published in ACM venues across all of computer science. |
| Dr June Andronick gives SUE talk about how industries should start switching to verified software |
|
2018-01-30 "Trust Your Software?" - Trustworthy Systems'
group leader June Andronick has given a SUE Talk as part of
the Monash Business School executive education program
'Your Leadership Voice: Women in Focus'. SUE talks are
bold, passionate and inspiring talks by
successful, unstoppable
and empowering women changing the face of
business! You can learn more about the 'Your Leadership
Voice: Women in Focus' program here.
|
| Meltdown-Spectre amplifies call for new hardware-software contract |
|
2018-01-29 Gernot Heiser's call for a new hardware-software
contract has been amplified by the revelations of the
Meltdown-Spectre attacks. ZDNet wrote an article interviewing Gernot about the current issues with the ISA and what needs to be done to help mitigate these attacks in the future. Read the article here. Gernot's paper on the the Hardware-Software contract: "For Safety’s Sake: We Need a New Hardware-Software Contract!" can be found here, as well as a more layman-friendly article published in the Conversation titled "Insecure by design – lessons from the Meltdown and Spectre debacle" can be found here. |
| Bad benchmarks bedevil boffins' infosec efforts |
| 2018-01-16 'Benchmark crimes' understate true performance impact of security controls. Gernot Heiser recently spoke to the Register to discuss their paper about how researchers can sometimes use misleading or inaccurate numbers in measuring the performance of their software. Read the Register article here. |
| CDDC wins two national iAwards |
| 2017-08-31 The Cross-Domain Desktop Compositor (CDDC) is a fruitful collaboration of Trustworthy Systems with DST Group. After having won three state-level iAwards in South Australia earlier in the year, it has now won the national awards in the categories Infrastructure & Platforms Innovation of the Year and Research & Development Project of the Year. The iAwards are an annual program of the Australian Information Industry Association (aiia) that recognises and rewards technology innovations that have the potential to, or are already having, a positive impact on the community. |
| Congratulations to Dr. Legg! |
| 2017-07-04 Alex Legg has been awarded his PhD for his thesis entitled "A Counterexample Guided Method for Reactive Synthesis". Alex is now working for Google. |
| Ramana Kumar has won the John C. Reynolds Doctoral Dissertation Award |
| 2017-07-03 Ramana Kumar has been awarded the very prestigious John C. Reynolds Doctoral Dissertation Award for his PhD. It is awarded annually to the author of an outstanding doctoral dissertation in the area of programming languages. You can read more about the award and Ramana's thesis here. |
| Trustworthy Systems in the news |
| 2017-06-29 Gernot Heiser has been interviewed about the work of Trustworthy Systems and seL4 by LifeHacker. See the article here. |
| CDDC wins iAwards |
| 2017-06-16 The CDDC has won three iAwards! The Cross Domain Digital Compositor is a joint project with the DSTG, and it won three major iAwards at the ceremony on 15th June. Read our blog post about it here. |
| Successful final DARPA HACMS demo |
| 2017-04-03 The DARPA HACMS program had a successful final demo day near Washington, to a few hundred industry and government folks. Our seL4 microkernel was at the core of everything demoed, including a a Boeing optionally-piloted helicopter, an autonomous US Army truck and a smart helmet for Army soldiers that Rockwell Collins developed and is trying to sell to the ADF. There were life hacking demos on research vehicles, and videos from life hacking demos of the military vehicles (including an in-flight attack on the helicopter). |
| seL4 in spaaaace! |
| 2017-03-28 A rocket carrying the UNSW QB50 Qubesat was successfully launched to the International Space Station. The satellite, which carries an seL4-based experiment, will be launched onto orbit in May |
| Gernot Heiser to give a keynote at Embedded Systems week |
| 2017-03-24 Gernot Heiser to give a keynote at Embedded Systems week |
| Gernot Heiser will teach on operating systems for secure and safe embedded systems at the HiPEAC International Summer School |
| 2017-02-21 Gernot Heiser will teach on operating systems for secure and safe embedded systems at the HiPEAC International Summer School on Advanced Computer Architecture and Compilation for High-Performance and Embedded Systems (ACACES '17) |
| Fifth Data61 Software Systems Summer School |
| On February 13 and 14, 2017, the 5th Software Systems Summer School will be held at UNSW. PhD Students and their supervisors from around Australia are invited to take part. |
| Fellow of the Association for Computing Machinery (ACM) |
| Professor Steve Blackburn from the Australian National University (ANU) Research School of Computer Science has been placed among the world’s best computer scientists, after being named a Fellow of the Association for Computing Machinery (ACM). In total, 53 ACM members were elevated to Fellow level in 2016, with Professor Blackburn joining Professor Gernot Heiser and between them they make up 2/3 of all the ACM Fellows currently employed in Australia More |
| Australian Academy Of Technology and Engineering Fellows for 2016 |
| Gernot Heiser has also been elected one of the twenty-five new Australian Academy Of Technology and Engineering Fellows for 2016. |
| ICT Researcher of the Year award Nov 2016 |
| Gernot Heiser won the ICT Researcher of the Year award of the South-East Asia Regional Computer Confederation (SEARCC) at the Re-imagination Summit in Sydney More |
| GovHack 2016 Awards |
| Research Assistant Felix Kam's team of 6 won 3 awards at GovHack 2016 sponsored by Google, the ATO and the ABS, with cash prizes totaling $7000. Their project TaxLess: optimizing your tax returns, won first prizes of the Machine Learning Hack, Smarter Data and Data intelligence awards. GovHack is the largest open government and open data hackathon in Australia, where 3000+ participants competed across 40 locations and submitted 480 projects. |
| Trustworthy Systems wins 1st and 2nd place in SYNTCOMP’16 |
| The Trustworthy Systems group placed first and and second in the international SYNTCOMP’16 Reactive Synthesis Competition. Synthesis is an approach to software correctness where programs are automatically generated. The tool “Simple BDD Solver” by Adam Walker came first in the sequential realisability track - for the third year in a row, and the the tool “TermiteSAT” by Alexander Legg came second in the parallel realisability track. Both tools come out of Data61’s Trustworthy Systems research in enhancing operating system reliability by automatically synthesising device drivers. |
| Call for TASTE OF RESEARCH (TOR) Projects 2016/2017 |
| The submission of projects for the UNSW Taste of Research program for 2016/17 are due May 20th 2016... |
| Outstanding paper award at RTAS '16 |
| PhD student Thomas Sewell presented the 'Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis' paper at RTAS'16 which took place at CPS week in Vienna. The work won an outstanding paper award at RTAS |
| IEEE Trans Computers (TC)- Gernot Heiser |
| IEEE Fellow Gernot Heiser has been appointed associate editor of IEEE Trans Computers (TC)...more |
| L4 Microkernels Published |
| The paper ‘L4 Microkernels: The Lessons from 20 years of Research and Deployment’ was published in ACM Transactions on Computer Systems. Authors Senior Principal Researcher Gernot Heiser and Principal Researcher Kevin Elphinstone |
| Software Systems Summer School 8th – 9th February 2016 |
|
NICTA is again running its Software Systems Summer School
this coming February in Sydney, with a number of
high-profile international speakers. The summer school will cover a range of issues in systems (operating systems, hypervisors, virtual machines, computer architecture,cloud computing, databases, compilers, language implementation, memory management and security). It follows the same general model as the highly successful summer school we held in the previous three years. |
| Seminar 2016-02-05: Douglas Carmean - What Could Possibly go Wrong? A Look at the Dark Side of Computer Architecture |
|
A clear market need, compelling usage models and a dream
team create the perfect storm for a fantastically
successful product. Compromises, unforeseen challenges and
poor decision making can conspire to turn a brilliant
product into a merely successful endeavor. This talk will explore the underbelly of computer architecture and product definition. It will look at things that went wrong and lessons learned from the execution of a major product development. While the scope of the project was to create new business opportunities in excess of $1B, some of the lessons are surprisingly applicable to everyday computer architecture projects. |
| Gernot Heiser — IEEE Fellow 2016 |
| Congratulations to Gernot Heiser for being named an IEEE Fellow, commencing in 2016. This is a distinction reserved for select IEEE members whose extraordinary accomplishments in any of the IEEE fields of interest are deemed fitting of this prestigious grade elevation..more |
| Gernot Heiser named ICT Researcher of the Year |
| Congratulations goes to Gernot Heiser on receiving the 2015 Digital Disruptor - ICT Researcher of the Year in what was an extremely competitive category..more |
| Seminar 2015-11-16: Professor Gene Tsudik - Scalable Embedded Device Attestation |
| Today, large numbers of smart interconnected devices providesafety and security critical services for energy grids, industrial controlsystems, building automation, transportation, and critical infrastructure. These devices often operate in groups, forming large, dynamic, and even self-organizing, networks. Collective integrity verification of software for device groups is necessary to ensure their correct and safe operation as well as to protect them against malware infestations. However, current device attestation schemes assume a single prover and do not scale to groups thereof. We discuss the design of SEDA -- the first attestation scheme for device groups. This work includes a formal security model for swarm attestation and two proof-of-concept SEDA implementations based on two recent attestation architectures for embedded systems. SEDA can efficiently attest device groups with dynamic or static topologies. |
| Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System |
| This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers. |
| 2015-09-01 Google PhD fellowship |
| Congratulations to PhD student Qian Ge who has won a Google PhD fellowship with Research Proposal Title: Low Overhead Operating System Mechanisms for Eliminating Microarchitectural Timing Side Channels |
| 2015-08-17 Best Scientific Cybersecurity Paper Award Winner |
| Congratulations to TS's Prof Carroll Morgan and co-authors, who have won the Annual NSA Best Scientific Cybersecurity Paper Award for their paper Additive and Multiplicative Notions of Leakage and Their Capacities published at last year's IEEE Computer Security Foundations Symposium. |
| Seminar Irene Moser on Vehicle Routing with working hour constraints |
| The vehicle routing problem has been investigated for decades. Most approaches attempt to solve a standard formulation of the problem with few constraints. More recently, studies that accommodate loading constraints and delivery time windows have started to appear. In most cases, the objective is to minimise the total travel distance, travel time or the number of vehicles used. The implicit goal is to load a truck 'to the brim', to avoid frequent returns to the depot. In an actual case brought to us by industry, one of the important goals is to adhere to the maximal number of daily working hours a driver is available for. This means that in some cases, optimally loaded trucks are undesirable because they take too long for a driver to deliver legally. Consequently, the problem has been formulated in a different way for the solutions to be applicable in practice |
| Seminar: Mohan Baruwal Chhetri on Smart CloudBench - Performance Benchmarking of Black Box Cloud Infrastructure |
| Enterprises considering migration of their IT systems to the cloud only have a black box view of the offered infrastructure. While server pricing and specification information is publicly available, there is limited information about the underlying infrastructure performance. This makes comparison of alternative cloud infrastructure offerings difficult because cloud vendors use heterogeneous hardware resources, offer different server configurations, apply different pricing models and use different virtualization techniques to provision them. One way to evaluate performance of available cloud infrastructure alternatives is to benchmark the performance of software systems deployed on the top of the black box cloud infrastructure. However, this process can be complex, time-consuming and expensive, and cloud consumers can greatly benefit from tools that can automate it. Smart CloudBench is a generic framework and system that offers automated, on-demand, real-time and customized benchmarking of software systems deployed on cloud infrastructure. It provides greater visibility and insight into the run-time behavior of cloud infrastructure, helping consumers to compare and contrast available offerings during the initial cloud selection phase, and monitor performance for service quality assurance during the subsequent cloud consumption phase. In this presentation, I will first discuss the rationale behind the Smart CloudBench approach for benchmarking black box cloud infrastructure. Then, I will present a generic architecture for benchmarking representative applications on the heterogeneous cloud infrastructure and describe the Smart CloudBench benchmarking workflow. I will also present simple use case scenarios that highlight the need for tools such as Smart CloudBench. |
| Seminar 2015-08-25: Huan Nguyen on Rule-Based Extraction of Goal-Use Case Models from Text |
| Goal and use case modeling has been recognized as a key approach for understanding and analyzing requirements. However, in practice, goals and use cases are often buried among other content in requirements specifications documents and written in unstructured styles. It is thus a time-consuming and error-prone process to identify such goals and use cases. In addition, having them embedded in natural language documents greatly limits the possibility of formally analyzing the requirements for problems. To address these issues, we have developed a novel rule-based approach to automatically extract goal and use case models from natural language requirements documents. Our approach is able to automatically categorize goals and ensure they are properly specified. We also provide automated semantic parameterization of artifact textual specifications to promote further analysis on the extracted goal-use case models. Our approach achieves 85% precision and 82% recall rates on average for model extraction and 88% accuracy for the automated parameterization. |
| Seminar 2015-08-20: Florian Daniel; Recommendation and Weaving of Reusable Mashup Model Patterns for Assisted Development |
| Mashups are composite applications developed starting from reusable data, application logic and/or user interfaces, for example, sourced from the Web. Mashup tools are IDEs for mashup development that aim to ease mashup development, typically via model-driven development paradigms. This talk reports on recent research outcomes that aim to answer one of the problems proper of the mashup domain, that is, the lack of modeling expertise. This kind of knowledge is generally neither intuitive nor standardized across different tools, and the consequent lack of modeling expertise affects both skilled programmers and end-user programmers alike. The talk shows how to effectively assist the users of mashup tools with contextual, interactive recommendations of composition knowledge in the form of reusable mashup model patterns. It describes the design and performance study of three different recommendation algorithms and a pattern weaving approach for the one-click reuse of model patterns inside model-driven mashup tools. It discusses the implementation of suitable pattern recommender plugins for three different mashup tools and demonstrates via user studies that recommending and weaving contextual mashup model patterns significantly reduces development times in all three cases. The approach is of general nature and can easily be tailored to other model-driven development environments. |
| Seminar;2015-08-19: Gorka Irazoqui on Prevention of microarchitectural side channel attacks in the cloud |
| Side channel attacks have shown to be a potential thread for co-resident virtual machines in cloud computing environments. Among all, last level cache side channel attacks have proved to be the most powerful ones, being able to extract fine grain information such as cryptographic keys. Due to the increasing success of these kind of attacks, protections have to be implemented against them. In this work, we are building a tool that can mitigate side channel attacks in cloud environments. This is implemented in two steps: first, an identification phase where we detect that a malicious VM is running a side channel attack, and second, mitigate the attack by changing the memory layout of the malicious VM. For the identification phase, Hardware Performance Counters will be analysed looking for expected patterns for cache side channel attacks. In the mitigation phase, we will move malicious VM's memory pages to form a moving target defence. Although the tool will be applied to detect cache based side channel attacks, we believe it could also be adapted to detect microarchitectural attacks that use different hardware resources. This is work in progress. |
| Seminar 2015-08-19:Tom Allan; Mobile code cache-based side-channel attacks |
|
Side-channel attacks have been shown to leak cryptographic
keys. However, for the attack, the adversary needs access
to the physical machine the victim executes on. So, the
question is how does the adversary gets her code to the
victim machine. Web-based mobile code provides an easy
vector for getting code to the target machine, however
there are several hurdles for implementing such attacks
from mobile code. The first hurdle is that the attack code executes within a virtual address space which hides the mapping of the cache. Past research relies on huge pages to recover this mapping, however huge pages are not available to mobile code. We describe a cache profiling technique that allows us to profile the cache without the use of huge pages. Another hurdle is that cache-based attacks rely on a high-resolution timer. As a precaution against cache-based attacks, browsers are now moving towards disabling high-resolution timers. We demonstrate that we can create a high-resolution timer by using multiple threads. Lastly, prior cache-based attacks focused on statically-compiled languages. With the move to the Web, many programs are now written in dynamic languages. Consequently the memory layout of the program is unknown to the adversary. We show that implementations in dynamic languages are still vulnerable. We implement the attack code in both Javascript and as Google Chrome's Native Client. We use the attack against the Javascript ElGamal encryption as implemented in Openpgp.js and show that using the side channel information we can reduce the search space to 2^30 keys. |
| Seminar 2015-08-18: Harry Butterworth on Paxos In Production |
| The core of IBM's Spectrum Virtualize(TM) software is a Paxos-based, fault-tolerant cluster operating environment which has been in production use since 2003. In the context of multinational enterprise IT infrastructure, I will first introduce some current storage products powered by IBM Spectrum Virtualize(TM) software, then I will review fault-tolerance and the Paxos protocol and finally I will describe a programming model, protocol extensions, supporting features and optimizations used in this deployment of Paxos in production. |
| Seminar 2015-08-17: Jan Auer; Enhancing Static Analysis with Runtime Verification |
| Static program analysis and runtime verification are two complementary, yet supplemental approaches to ensuring correct program execution. Theformer is well established and integrated in many development environments, as well as several enterprise-grade standalone tools. Runtime verification, on the other hand, facilitates targeted monitoring of production systems without the risk of false positives or false negatives. In this presentation we preset "Static Runtime Verification", a formalbridge between static analysis and runtime verification that leverages synergy effects between both approaches. Analysis comprises three stages: Identification of error candidates using static analysis, event instrumentation at these locations, and final runtime monitoring. Moreover, we introduce our prototype platform StaticRV and a number of use cases |
| SYNTCOMP 2015 |
| Adam Walker wins the synthesis competition again this year in his category Sequential realizability More: |
| Seminar 2015-07-06: Prof. Cesare Pautasso; Let's have a RESTful Conversation |
| The REST architectural style has made a strong impact on the way Web services are designed, built and also composed. In this talk we take a close look at the way clients interact with them and introduce the notion of RESTful conversation. We show that there many examples of recurring conversation types that can be found on the Web (from small indirect lookups based on hypermedia relationships, to the navigation within the elements of collection resources or the confirmation/cancellation of reserved resources within RESTful atomic distributed transactions). Capturing them helps to raise the abstraction level when modeling RESTful APIs and also provides a novel perspective to study the relationship between business processes and Web resources, or what we call RESTful Business Process Management. |
| Seminar 2015-06-30; Prof. Ryszard Kowalczyk on Enabling Smart Infrastructure with Intelligent Agent Technologies |
|
Smart infrastructure encompasses networked infrastructure that uses ubiquitous sensor, information and communication technologies to better utilise or sustain resources. Examples of smart infrastructure include electricity grids that improve grid reliability and better utilise energy; transport systems that optimise traffic flows; water networks that improve productivity in agriculture; and cloud computing that improves productivity and utilisation of ICT resources. Emerging uses of smart infrastructure have the potential to reduce costs, enhance safety and reduce our environmental footprint. In order to realize the full potential of smart infrastructure, new technology solutions are required to support smart data use, distributed coordination and decentralised optimisation across the infrastructure. In particular the talk will focus on enabling smart energy grids and smart cloud systems with intelligent agent technologies. It will include examples of on-going research on market-based demand-response control and agent-based management of self-sufficient micro-grids. Cloud computing examples will focus on smart cloud broker involving smart cloud bench, purchaser and marketplace |
| Seminar 2015-06-10; Stratos Idreos; Curious and self-designing systems: towards easy to use data systems tailored for exploration |
| How far away are we from a future where a data management system sits in the critical path of everything we do? Already today we need to go through a data system in order to do several basic tasks, e.g., to pay at the grocery store, to book a flight, to find out where our friends are and even to get coffee. Businesses and sciences are increasingly recognizing the value of storing and analyzing vast amounts of data. Other than the expected path towards an exploding number of data-driven businesses and scientific scenarios in the next few years, in this talk we also envision a future where data becomes readily available and its power can be harnessed by everyone. What both scenarios have in common is a need for new kinds of data systems which are tailored for data exploration, which are easy to use, and which can quickly absorb and adjust to new data and access patterns on-the-fly. We will discuss this vision and some of our recent efforts towards self-designing systems as well as "curious" systems tailored for automated exploration. |
| Seminar 2015-06-04: Onur Mutlu; Rethinking Memory System Design for Data-Intensive Computing |
| The memory system is a fundamental performance and energy bottleneck in almost all computing systems. Recent system design, application, and technology trends that require more capacity, bandwidth, efficiency, and predictability out of the memory system make it an even more important system bottleneck. At the same time, DRAM and flash technologies are experiencing difficult technology scaling challenges that make the maintenance and enhancement of their capacity, energy-efficiency, and reliability significantly more costly with conventional techniques. |
| Seminar 2015-05-19; James Zheng on Physically Informed Runtime Verification for Cyber Physical Systems |
|
Cyber-physical systems (CPS) are an integration of computation with physical processes. CPS have gained popularity both in industry and the research community and are represented by many varied mission critical applications. Debugging CPS is important, but the intertwining of the cyber and physical worlds makes it very difficult. Formal methods, simulation, and testing are not sufficient in guaranteeing required correctness. Runtime Verification (RV) provides a perfect complement.However, the state of the art in RV lacks either efficiency or expressiveness, and very few RV technologies are specifically designed for CPS. In this talk, I discuss a toolset, which brings formal methods (e.g., temporal logic and time automata) and physical models (through real time simulation) into CPS runtime verification. The toolset is evaluated through increasingly complex real CPS applications of smart agent system |
| Seminar 2015-05-15; Matthew Grosvenor ; Queues don't matter when you can Jump them! |
| In this talk I will be discussing our recent system called QJump. QJump is a simple and immediately deployable approach to controlling network interference in datacenter networks. Network interference occurs when congestion from throughput-intensive applications causes queueing that delays traffic from latency-sensitive applications. To mitigate network interference, QJump applies Internet QoS-inspired techniques to datacenter applications. Each application is assigned to a latency sensitivity level (or class). Packets from higher levels are rate-limited in the end host, but once allowed into the network can “jump-the-queue” over packets from lower levels. In settings with known node counts and link speeds, QJump can support service levels ranging from strictly bounded latency (but with low rate) through to line-rate throughput (but with high latency variance). We have implemented QJump as a Linux Traffic Control module. QJump achieves bounded latency and reduces in-network interference by up to |
| Seminar 2015-05-15; Matthew Grosvenor ; Atomic Broadcast for the Rack-Scale Computer |
| Atomic Broadcast is a powerful primitive for implementing agreement systems. The way in which atomic broadcast is implemented depends on the underlying communications infrastructure. Multiprocessors can assume the presence of special purpose, low latency and highly reliable interconnects giving rise to systems that operate in just a few CPU cycles. Whereas, across machine boundaries the communication infrastructure is typically general purpose, higher latency and less reliable. In these situations more complex software approaches such as Paxos, Raft and Zookeeper Zab are used. As a consequence, atomic broadcast between machines is slow and scales poorly. The racks-scale computer (RSC) falls somewhere between these two worlds. Although constructed out of unreliable sub-components, we would like to be able to treat the machine as if it were a single unit. Our work is motivated by this apparent contradiction, and the observation treating the rack as a single machine provides us with an opportunity to build custom interconnects using general purpose components. In this talk I will discuss Exo, a fast and efficient network architecture and protocol for atomic broadcasts at the rack scale. Exo builds upon the well established theory of token-ring based atomic broadcast protocols. The Exo protocol is accelerated using a specialised low latency network architecture and a custom hardware acceleration engine. The network is constructed from commodity Ethernet networking components and the acceleration engine is programmed into commodity FPGA enabled network cards. Exo is a work in progress. At time of writing, the Exo protocol is running in our lab on a small test cluster of15 nodes. Currently the system is capable of a sustained rate of over 2 million messages per second and coping with transmission faults (bit-errors), arbitrary partitions and failing nodes. We expect that over the coming months this will mature into a fully featured system, capable of operating several orders of magnitude faster, and with at least an order of magnitude greater scale than existing systems. |
| Seminar 2015-05-12; John Grundy on The Future of Software Engineering in Australia |
| Professor John Grundy is Dean of the School of Software and Electrical Engineering at Swinburne University of Technology. He is also Director of the Swinburne University Centre for Computing and Engineering Software Systems (SUCCESS). His teaching is mostly in the area of team projects, software requirements and design, software processes, distributed systems, and programming. His research areas include software tools and techniques, software architecture, model-driven software engineering, visual languages, software security engineering, service-based and component-based systems and user interfaces. John will be giving a talk on The Future of Software Engineering in Australia. In this talk John will outline what he considers to be key issues for software engineering research and practice in Australia. He will highlight some key example areas we are working in to address these in our research group. |
| CeBIT 2015 |
| Australia's leading technology & business expo is here in Sydney 5-7 May, 2015. 450 exhibitors from Australia and around the world – from startups to multinationals – showcase their innovations and technologies on the CeBIT Expo show floor. SSRG will be represented by Trustworthy Systems displaying the quadcopter and talking about HACMS/SMACCM. |
| Seminar 2015-05-01; Philipp Hoenisch on [Auto-Scaling²] - Optimizing Docker Placement on VMs |
| Lightweight containers, and most recently Docker containers, are getting more and more attention by developers and sysadmins. Similar to Virtual Machines (VMs), Docker provides an additional abstraction aiming at sharing underlying resources and libraries. Complex applications can be bundled and configured in images and then easily be deployed on any host. The big advantage of using Docker containers over VMs is the reduced system overhead as no additional operating system needs to be started. This enables hosting more independent applications on one single host. However, since computing resources (CPU, RAM, ...) are shared among the containers, a single container requiring too many resources may lead to unwanted side effects to other containers on the same host. Auto-scaling is now more complex as the research question becomes of how to place Docker containers on certain VMs under a given workload in order to prevent over- and under-provisioning. In his current work, Philipp addresses this topic by devising a two layer scaling approach using a multi-objective optimization model. |
| Rob van Glabbeek joins Royal Holland Society of Sciences and Humanities |
| Rob van Glabbeek has been selected as a foreign member of the Royal Holland Society of Sciences and Humanities, a Dutch organisation founded in 1752 to to promote science in the broadest sense. Members are nominated by invitation only, based on their scientific achievements. So far 19 computer scientists have been awarded a membership |
| Seminar 2015-03-10 |
| Jean-Baptiste Jeannin - CMU - gave a talk on Differential Temporal Dynamic Logic for Hybrid Systems and Airplane Collision Avoidance. In this talk, Jean-Baptiste Jeannin presents a new logic, the differential temporal dynamic logic dTL2, to express temporal properties about Cyber-Physical Systems. He then shows an application to airplane collision avoidance, with a verification of the next-generation Airborne Collision Avoidance System (ACASX), currently being developed by the Federal Aviation Administration (FAA). |
| 2015-02-19 Techfest |
|
NICTA’s Techfest showcase’s over 30 technology
demonstrations, including highly secure operating systems
for drones, vision processing systems for Australia’s
bionic eye, map-based access to open spatial data, and
unique 3D GPS tracking software featuring synchronised
sound and video. The Hon. Malcolm Turnbull, Federal Minister for Communications opened the event. |
| 2015-02-09 Summer School |
| The 3rd Software Systems Summer School featured lectures by international leaders in computer systems from industry and academia, interspersed with short student talks. The emphasis was a friendly and informal setting where students learn and obtain feedback from experts. Sessions included Distributed Data, Search and Software Systems, Managed Language Implementation, Performance Analysis, Security and supporting Real-Time Applications, Trust and Safety and Big Data. |
| 2015-01-15 Workshops |
| Senior Researcher Toby Murray presented at Core Infrastructure Workshop in London and also presented seL4 security workshop at Oxford Uni and Imperials College, London. Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems |
| 2015-01-06 — Summer Camp |
| A new SSRG initiative, the Software Summer Camp (SSC) ran 9 high-performing first-year students running from early January to mid Feb. Targeted at students with little or no pre-university programming experienced, the summer camp gives students additional experience building software-systems for real use. The aim is to build students’ confidence, especially targeting members of under-represented groups. Students worked in groups to build embedded systems, which are now being used at NRL. The experiment was considered a success by all participants and will be repeated next summer, with improvements based on what we learned from the trial |