Discovery Early Career Researcher Award - Grant ID: DE130100292
Funder
Australian Research Council
Funding Amount
$285,000.00
Summary
Towards a stronger proof system for combinatorial optimisation. Combinatorial optimisation problems such as staff rostering, vehicle routing or resource allocation are central to the efficiency of many businesses and industries. This project will improve optimisation technology by using the low-level structure of the problems to find better solutions. This will save time, money and reduce environmental impact.
Robust and Scalable Autonomous Landing for Drones. The aim of this project is to develop a transformative robust and scalable autonomous landing system for drones. This is the critical missing technology needed to unleash exponential growth in a potentially enormous drone delivery industry by enabling a multitude of applications to deliver goods and supplies via drones to a wide range of destinations in Australia and the world in a timely, flexible and accurate manner. Such an autonomous landi ....Robust and Scalable Autonomous Landing for Drones. The aim of this project is to develop a transformative robust and scalable autonomous landing system for drones. This is the critical missing technology needed to unleash exponential growth in a potentially enormous drone delivery industry by enabling a multitude of applications to deliver goods and supplies via drones to a wide range of destinations in Australia and the world in a timely, flexible and accurate manner. Such an autonomous landing solution would revolutionise drone technology, and propel Australia to the forefront of technology innovation. This project would benefit not only large scale delivery by drone in urban and suburban areas of Australia but also long distance delivery via drone to remote areas of Australia.Read moreRead less
Provable elimination of information leakage through timing channels. 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 ....Provable elimination of information leakage through timing channels. 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.Read moreRead less
Design and verification of correct, efficient and secure concurrent systems. This project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. Computers with multiple processors are now the norm and are used in a wide range of safety, security and mission critical software applications such as transport, health and infrastructure. These multi-core architectures have the potential to lead to important effici ....Design and verification of correct, efficient and secure concurrent systems. This project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. Computers with multiple processors are now the norm and are used in a wide range of safety, security and mission critical software applications such as transport, health and infrastructure. These multi-core architectures have the potential to lead to important efficiency gains, but can introduce complex and error-prone behaviours that cannot be managed using traditional software development approaches. This project will produce better, scalable and mechanised methods for the design and verification of such software which is expected to reduce the prevalence of failures in efficient, modern software.Read moreRead less
Structure of relations: algebra and applications. Relations and relational structures form the fundamental mathematical essence required for studying computational problems and computational systems. This project will provide new algebraic methods for solving old problems in the theory of relations, informing our understanding of computational complexity and the nature of computing.
Automatic software verification: harnessing constraint technologies. As we come to rely on software to manage more and more aspects of our lives, the importance of software reliability increases; yet as programs become increasingly complex, reliability becomes ever more elusive. This project will develop automated tools and techniques to ensure that programs do what they were intended to do.
Analysing Computer Arithmetic to Improve Software Reliability. Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software deals with idealised mathematical integers, since this simplifies reasoning significantly. In reality, most programs work with integer number representations that approximate the ideal. This compromises the soundness of many verification tools. This project will design sound reasoning tools that ....Analysing Computer Arithmetic to Improve Software Reliability. Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software deals with idealised mathematical integers, since this simplifies reasoning significantly. In reality, most programs work with integer number representations that approximate the ideal. This compromises the soundness of many verification tools. This project will design sound reasoning tools that are aware of the true nature of computer integer arithmetic.Read moreRead less
More information for better utility; less information for better privacy. More information for better utility; less information for better privacy. The contradiction is everywhere in contemporary IT: doctors need accurate information for diagnosis, but insurance companies' access should be limited; on-line retailers use your postcode to present interesting products, but they also deduce from it how much you will pay. One way to manage this contradiction is to tolerate "small" information flows p ....More information for better utility; less information for better privacy. More information for better utility; less information for better privacy. The contradiction is everywhere in contemporary IT: doctors need accurate information for diagnosis, but insurance companies' access should be limited; on-line retailers use your postcode to present interesting products, but they also deduce from it how much you will pay. One way to manage this contradiction is to tolerate "small" information flows providing the risks involved can be accurately gauged. This project will build on recent advances in information measuring to develop new techniques for measuring the extent to which computer systems can defend against threats to privacy. Success in this project will lead to completely novel methods for security analysis of on-line applications where privacy is a critical issue.Read moreRead less
Artificial intelligence meets wireless sensor networks: filling the gaps between sensors using spatial reasoning. Monitoring potential disaster regions and integrating available information with expert knowledge can prevent disasters and save many lives. The outcome of our project is one of the key components for intelligent systems that can autonomously monitor the environment, make the correct inferences and issue appropriate warnings and recommendations.
An extensible framework for analysis of Java language-based security conformance. Java is a programming language and platform running on 3 billion devices. While Java provides a sandbox-based security architecture within the Java Class Library to protect systems from untrusted code downloaded from Internet, it cannot defend against implementation bugs that occur in the Java Class Library. The goal of this project is to provide a formal model of the Java security architecture, which can be used b ....An extensible framework for analysis of Java language-based security conformance. Java is a programming language and platform running on 3 billion devices. While Java provides a sandbox-based security architecture within the Java Class Library to protect systems from untrusted code downloaded from Internet, it cannot defend against implementation bugs that occur in the Java Class Library. The goal of this project is to provide a formal model of the Java security architecture, which can be used by program analysers to identify faulty or insufficient security checks in the Java Class Library that may lead to the sandbox being bypassed.Read moreRead less