Details of Grant 

EPSRC Reference:	EP/Y003535/1
Title:	TYPDSEC: TYPe-based information Declassification and its SEcure Compilation
Principal Investigator:	Rajani, Dr V
Other Investigators:
Researcher Co-Investigators:
Project Partners:	Chalmers University of Technology DPella
Department:	Sch of Computing
Organisation:	University of Kent
Scheme:	Standard Research - NR1
Starts:	01 December 2023	Ends:	30 November 2025	Value (£):	160,392
EPSRC Research Topic Classifications:	Computer Sys. & Architecture
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:	Panel Date Panel Name Outcome 17 May 2023 ECR International Collaboration Grants Panel 1 Announced
Summary on Grant Application Form
Programming with confidential data is ubiquitous in the modern world. For instance, imagine using credit card information for e-commerce, and passwords or private keys for authentication. Bugs in secret-handling code can cause information leaks, revealing sensitive, private information to untrusted parties. Corporations often spend huge amount of resources. to ensure the secrecy of the data being handled by the program. Despite all this, time-and-again attackers manage to get hold of sensitive information, for instance, by exploiting untested paths or bypassing the deployed security enforcement. The average data breach was estimated to cost USD 4.35 million in 2022. This raises several fundamental questions, like 1) What does it mean for a program to be secure in a formal sense?; 2) Can we express confidentiality policies on data being programmed?; 3) Can we build methods to provide formal security guarantees wrt such confidentiality policies? and 4) Finally, can we ensure that such security guarantees are preserved even after compilation? (i.e. argue that the compiler itself has not introduced a covert channel thwarting the guarantees offered before compilation)? The proposal aims to answer the questions like above by building methods and tools for providing provable guarantees about program confidentiality (even in the presence of deliberate information disclosure, as is often required in practice). The proposed work aims for two key deliverables 1. A programming language in which every program is provably secure by construction. 2. A compiler that ensures that security guarantees are preserved even after compilation.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.kent.ac.uk