Certifying the correctness, security and reliability of software: Swarn Priya wins L'Oréal-UNESCO 2023 prize

The aim of Swarn Priya's research is to certify the accuracy of software and ensure that it does not leak sensitive information by indirect means, using formal methods. Software development covers a wide range of fields, including cryptography, blockchain and mission-critical systems. During the design and development process, it is possible to make errors or oversights, which can create vulnerabilities or loopholes for unauthorized activities within the software, potentially leading to serious consequences. These can include loss of life in the case of air traffic control systems, financial loss in the case of financial software, leakage of sensitive data in the case of cryptographic systems, and so on. An attacker can gather information on software secrets by observing its side effects, such as energy consumption or execution time. These malicious activities are possible even when the software is correctly implemented, and can lead to serious security breaches.

This is Swarn Priya's area of expertise. Certification of correctness and assurance of security against attackers are provided using machine-verified proofs. Her doctoral work led to the construction of a correct and secure software system, protected against temporal attacks. Temporal attacks are exploits in which an attacker recovers secret information by analyzing the execution time of the software, even though it has been implemented in a functionally correct way.

Designing and executing verification is a manually intensive task, requiring the learning of a new domain-specific language. The threat model is constantly evolving, and new models need to be built or existing ones adapted on an ongoing basis to support them, with a framework that is as generic as possible to handle new changes.

The long-term challenges for Swarn Priya's research field are to raise awareness of the importance of formal methods and to find ways of reducing their complexity during their applications. It's not easy to integrate formal method techniques into an existing software system. This leads to the challenge of promoting and including them early on in software development cycles, and to have tools that automate the process of building formal software models and automating proofs. This would enable people with little knowledge of formal methods to rely on these tools to certify their software.

The challenge of building correct and secure software systems has applications in a wide range of fields, from autonomous vehicles and robotics to mission-critical systems and cryptography, guaranteeing compliance and security. The results of her research are applied to cryptography and cybersecurity, mainly in designing of secure protocols by incorporating formal methods into the software development cycle to ensure the development of accurate and secure systems that effectively counter temporal attacks, thus preventing the potential exposure of secret data.

Originally from Bihar in India, Swarn Priya was confronted with gender stereotypes and discrimination. From an early age, girls are taught that they should succeed in caring for their families rather than in professional life. While the promotion of girls' education has come a long way since the past, there is still a long way to go. Despite the support of her family, society's cultural norms hampered her dream of pursuing a career as a woman scientist, and she had to leave her family and go abroad to realize her dreams.

Increased representation of women in science, as enabled by the L'Oréal Foundation's "Young Talents" program, encourages young women to pursue their scientific careers. It also dismantles stereotypes and combats sexist discrimination, fostering a more inclusive environment for women. Financially, it enables them to gain financial independence and encourages them on their path to success.

This recognition is fundamental for Swarn Priya. The program will enable her to meet other talented women who have succeeded in the scientific field, and to make contacts that will lead to new collaborations and career opportunities. "It will give me confidence because my work will be recognized worldwide. It will help me become a role model for young girls at home and abroad. It will develop my skills and help me achieve my long-term goals."