Thesis Topic Details

Topic ID:
2960
Title:
Verification of Secure Transaction Protocols
Supervisor:
Ron van der Meyden
Research Area:
Security, Formal Methods, Databases
Associated Staff
Assessor:
Carroll Morgan
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
background in formal methods and databases, security beneficial
Description:
Multi-level secure databases seek to enforce information flow security
policies that proscribe the release of High level secrets (e.g.
military plans, intelligence agency information, employee salary data)
to a lower security level.

A body of research conducted in the late 1980's and early 1990's
showed that there is potential for insecure information leakage
when High level and Low level database transactions execute
concurrently. To address this problem,
a number of protocols for the management and
scheduling of secure concurrent transactions were proposed.
This area is likely to reemerge into significance in the context of
emerging transactional memory architectures for multicore processors,
which are seeking to use database transaction ideas such as
serializability and atomicity to provide programmers of multicore
systems with a more tractable conceptual model for concurrency.
See [C40] Access Control and Information Flow in Transactional Memory, A. Cohen, R. van der Meyden and L. Zuck, Workshop on Formal Aspects of Security and Trust, Malaga, Spain, Oct 9-10, 2008 at
http://www.cse.unsw.edu.au/~meyden/research/publications.html

Since the time this area was of interest to the database community,
our theoretical understanding of security has significantly improved,
as has our ability to formally verify complex protocols. The protocols
proposed in the literature have not been formally assessed with respect
to the improved understanding of security, and indeed, we know of cases
where they are incorrect.

The project would be to study the formal verification of a protocol in this area, building a formal model and using either a proof tool or a model
checking tool to assess its correctness and security. Where errors are
found, this would open opportunities to develop corrected versions.
Both the verification and such corrections would be novel,
publishable results.


Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.