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. |
||