Skip to main content

News

News

CDDC wins two national iAwards
2017-08-31 iAwards logoThe 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) http://acaces.hipeac.net/2017/
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
Distinguished Paper Award at the 2016 OOPSLA Conference
Tony Hosking received a Distinguished Paper Award at the 2016 OOPSLA Conference. The paper, Hybrid STM/HTM for Nested Transactions on OpenJDK, was a collaboration with ANU, Purdue University, and the University of Massachusetts More
Most Influential Paper of 2016 Award
Steve Blackburn & Tony Hosking receive Object Oriented Programming, Systems, Languages and Applications (OOPSLA) Most Influential Paper of 2016 Award for The DaCapo benchmarks: Java benchmarking development and analysis paper. This is an award instituted by SIGPLANļ¼¨ACM’s Special Interest Group on Programming Languages formally ACM SIGPLAN Most Influential Paper of OOPSLA 2006. SIGPLAN awards only 4 of these awards each year, one for each of the major SIGPLAN conferences (POPL, PLDI, ICFP, OOPSLA). 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 More
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
University of Melbourne Early Career Researcher award October 2016
Toby Murray received an University of Melbourne Early Career Researcher award to pursue scaling up work on information flow with separation logic, the CompCert/Verified Software Toolchain (VST), and the Verasco verified static analyser.
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.
Endeavour Research Fellowship October 2016
Researcher Yuval Yarom has been awarded an Endeavour Research Fellowship to support his research into validating cryptographic implementations. The Endeavour Research Fellowships are Federal Government funded fellowships that provide Australian researchers with the opportunity for a 4-6 month research visit at an international institution. Yuval will be visiting Dr Nadia Heninger from U Penn in the coming year
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...more
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 SSRG'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 More..
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-31; Mark Staples on Critical Rationalism and Engineering
How does engineering support assurances about the use of critical systems? Engineering often uses science, but is engineering "scientific"? What is engineering, and how should we create and develop engineering knowledge? Does any of that matter to software engineering or computer science? (And are they a kind of engineering or science anyway?) When thinking about such questions, it would be good to have a better idea about what engineering is. Philosophy of Science is a well-established field. However, until recently there has been little work on the Philosophy of Engineering. In this talk I provide an overview of two recent papers about the nature and growth of engineering knowledge. I first discuss definitions of engineering, and note three recurring elements: the use of theories to show that designed artefacts meet requirements. I discuss some misconceptions about engineering, and contrast engineering theories with scientific theories. I then describe an ontological framework I have proposed for engineering knowledge. This adapts Karl Popper's well-known philosophy of Critical Rationalism (falsification and all that) and his less well-known Three Worlds ontology. The framework provides a basis for a taxonomy of falsification in engineering (a.k.a. engineering failure), and a taxonomy of responses to falsification in the growth of engineering knowledge.
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. more..
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-29 Len Bass retires
Len Bass retired from his full time work at NICTA and returned to the US but will maintain part time involvement. Len's research interests center around software architecture and its applications. Over the years, this has ranged from architecture evaluation, design, and documentation to supporting usability through software architecture to requirements elicitation to help define the software architecture to global software development to defining architecture related security controls for the smart grid.
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
2014-12-20 Gernot Heiser named ACM Fellow
Professor Gernot Heiser has been recognised as an ACM Fellow.
2014-12-13 Doctorate Awarded
Andrew Boyton’s PhD thesis has just been officially accepted, without changes from either reviewer and only 2.5 months after submission.
2014-11-30 MoU between NICTA and Augsburg University
Ralf Huuck facilitated the signing of an MoU between NICTA and Augsburg University
2014-12-05 — Visitors to NICTA and UNSW
Tony Hosking (Purdue) and Haibo Chen (Shanghai'TJ) visited UNSW and NICTA. Both gave seminars and met with staff and students
2014-11-25 Best student research paper award
David Cock won the CiSRA/CSE best student research paper award for his paper, ‘The last mile, an empirical study of timing channels on seL4’ with Qian Ge,Toby Murray and Gernot Heiser.
2014-11-22 Paper presented at Top Security Venue
David Cock presented his paper on analysing covert timing channels in seL4 at CCS, one of the top security venues
2014-11-17 German Chancellor Angela Merkel arrived at the National ICT Australia’s offices in Sydney
The German Chancellor and most powerful woman in the world had a host of post-G20 commitments in Sydney and chose to spend 45 minutes touring NICTA’s labs near Redfern. She was accompanied by Communications Minister Malcolm Turnbull and Industry Minister Ian Macfarlane during her tour of NICTA. more

...Older events

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.