Concurrent software is software that runs more than one thread simultaneously. Today, virtually all software applications are concurrent. Toby Murray (2018 IEEE Euro S&P) presented the first general purpose logic for proving information flow control security of shared memory concurrent programs. This lays a foundation for developing provably sound program analysis techniques for detecting and analysing vulnerabilities in concurrent software.
The logic, however, assumes that the software is data-race free and is therefore not affected by code optimisations made by the compiler or the multicore hardware. Furthermore, the logic assumes nondeterministic scheduling of threads by the operating system. These assumptions do not always hold. For example, programs may not be data-race free in order to improve efficiency (so called non-blocking algorithms are often used at the operating-system level) or simply due to poor design. Detecting vulnerabilities in such cases requires tools built on a logic that takes into account compiler and hardware optimisations.
Graeme Smith (2018 International Symposium on Formal Methods) has provided an operational semantics of program behaviour which takes into account optimisations made by hardware architectures including x86-TSO (Intel and AMD), ARM (ARM) and POWER (IBM). The long-term objective is to extend the foundations provided by these logics to cover all effects of hardware, operating systems and compilation processes on information flow analysis, to develop automatic program analysis tools that are built on them, and to integrate those tools within a secure software development process.
A short-term project would be to combine Smith’s semantics with the logic of Murray to provide a basis for program analysis tools which not only work with data-race free concurrent programs but also those relying on low-level non-blocking code, or with design errors leading to data races. Furthermore, semantics would be developed capturing the optimisations allowed by compilers (e.g., as defined for C and C++ by the C11 memory model) to similarly provide a basis for analysing higher-level source code. process.
This opportunity is open to all registered Australian Universities and Australian Publicly Funded Research Agencies.
Proposals submitted will be assessed equally on the following criteria:
Please limit submissions to no more than 2000 words. Ensure that all contact details, current and potential DST, Data61 collaborators and/or research partner details are on a separate page/covering sheet. The proposals will be de-identified during the selection process to eliminate any potential conflicts of interest.
Defence and Data61 reserves the right to fund all, some or none of the proposals received under this Call for Applications.
Successful applicants will be required to enter into a Data61 University Collaboration Agreement and a subsidiary Collaborative Research Project Agreement with Data61 in order to access project funding. Data61 will enter into contracts with the lead party in each proposal.
Any IP generated as part of the projects will vest in Data61 unless otherwise agreed, and Defence will receive a license for Commonwealth purposes only.
Any Commonwealth funding contributed to the projects will be paid in accordance with successful completion of milestones and as negotiated by the parties. Where circumstances necessitate it is possible for a small payment to be made upon execution of the agreement and in accordance with Defence procurement rules.
Please submit via the DST portal.
Proposals are to be submitted by 4.30pm Australian Eastern Daylight Time (AEDT), 15 August 2018. Only projects submitted via email to Cyber-NGTF@dst.defence.gov.au by the above deadline will be considered in this round.
For further information or assistance, please contact: