Karthik Bhargavan: proving the safety of web applications

Karthik Bhargavan uses squares, circles and arrows to explain the work that he'll be carrying out thanks to the five-year ERC grant of €1.5 million that he recently received. His field is computer security. "We exchange a lot of information online, so you need to be sure that it isn't stolen or altered ," explains this 34-year-old Indian researcher. "This is particularly true in certain sensitive areas such as banking and medical data. "

One example is digital medical records, which are set to be introduced in France and are already in use in the US. Each patient's data are encrypted and stored on a secure server, with certain individuals (the patient, the doctor, the hospital, etc.) having the right to read or add data. However, there are many potential targets for attack, including the web browser, the cryptographic protocol, the management of encryption keys, the programming of webpages (JavaScript programme), etc. So how is it possible to prove that the entire system is actually safe? How can we be certain that a hacker won't crack the protections put in place? This is the goal of the CRYSP project that was developed by Karthik Bhargavan and caught the ERC's attention. "Rather than stopping attacks, it's better to prevent them. My proposal is to build the first Web application whose security can be mathematically proven. The entire system has to be completely secure. "

Building the first Web application whose security can be mathematically proven

To mathematically prove that a computer program is safe, it first needs to be "converted" into a model that is easier to analyse. This model is then examined by a program analysis tool, which takes into account the security requirements chosen by the researchers. This tool can give three types of response: "yes, the safety of this software is proven", "no, attacks have been successful" and lastly "we do not know whether this software is safe" . Unfortunately, the latter response is the most frequent. Indeed, the goal of Karthik Bhargavan's research is to make this response less frequent and achieve the affirmative response more often.

Karthik Bhargavan is to recruit two post-doctoral researchers, four PhD students and seven Master's-level interns over the next five years to complete his project. This researcher with an international background (studies in New Delhi, India, a PhD from Philadelphia in the US and seven years of research on Web security at Microsoft Research in Cambridge, United Kingdom) is not at all concerned about the recruitment process: "I really like working with French students - I teach them at the École Polytechnique ," he says. "The quality of the students is one of the reasons why I chose France. I'm also planning to attract students from the US, the UK and India, where I've kept a lot of contacts. "

He also chose France and Inria for its unique combination of skills in engineering and mathematics, due in particular to the close collaboration between researchers at Inria and Microsoft Research at the joint laboratory in Saclay. "The combination of highly applied and fundamental research conducted at Inria is very attractive ," he notes. "I work both on programs and mathematical proofs. I'm also fortunate enough to be looking at real problems. "