“Modern societies are relying heavily, and to an ever-increasing extent, on a variety of machines to perform many fundamental tasks,” says Veltri, who studied mathematics at the University of Florence, in addition to postdoctoral research on the topic at the IT University of Copenhagen. “Since we have placed a lot of trust in these machines, we always assume that they function correctly. Occasional failures in these systems and machines can lead to both major financial losses and wider problems for society as a whole. For example, important security systems may be attacked, sensitive or personal information may be leaked, and vehicles with technical errors or incorrect programming may be exposed to the public.” 

The researcher adds that corresponding computer software has been developed to verify the correctness of most of these useful machines, ensuring their accurate and error-free operation. 

“Consequently, the systematic formal certification of hardware and software delivered worldwide is extremely important,” he says.  

“Certification ensures the reliable functioning of these systems, and an ever-increasing number of software developers are moving towards creating software aimed at the verification of software itself.” He adds that Estonian IT companies have also seen the need for high-assurance software and started to make developments in this direction. 

“This means increasing monetary investments in the departments and working groups that use formal methods to analyse, certify and control their own software products, including the software that is designed to analyse other programs being created,” explains Veltri. 

Developing software for program analysis 

Veltri’s research in the framework of the EXCITE project revolves around the development of methodologies for the formal verification of various computer systems, predominantly using various logical and mathematical techniques. 

“My tools are interactive theorem provers,” he explains. “These are highly expressive programming languages that can be used to encode many of the mathematical structures often used in computer science. With these, researchers in this field try to create specific mathematical models for computer systems, which in turn can be used to simulate and thereby predict the behaviour of these computer systems. As a result, we produce models that have been certified because their correctness and reliability have been proven by the machines themselves. This then gives the end user confidence that the system works correctly and is reliable.” 

Veltri adds that the idea of developing theorem provers and related languages that certify the correctness of programs is not new, but as our lives are becoming increasingly reliant on computers, the evident need for them has risen to a whole new level in recent times. The researcher adds that as computer systems are constantly becoming more complex and comprehensive, it is no longer possible for people to control all systems and lines of code themselves as it is also extremely expensive. However, machines can be employed as useful tools for attesting the correctness of these complex systems and programs. 

Veltri adds that the development of software for formal verification began as early as in the late 1960s, which at the time was more of a task for academic research. The need for theorem provers saw a significant surge in the 1990s as computers became more powerful, their use expanded into all walks of life, and companies began to suffer financial losses due to being unable to anticipate potential problems. Problems, for example, with the operation of new computer programming languages on new computers should they become many times more powerful in a few years, or the inverse issue of the operation of software, where new programs require much more power from their processors. 

“A key example is one of the world’s largest computer chip manufacturers, Intel, which produced tens of thousands of new processors which were discovered later, after production, to have a major flaw. The error occurred because they were unable to anticipate all possible errors in chip production. The employment of theorem provers in this case would have been able to detect such an error prior to the chip commercialisation, and the company could have been able to correct the issue. It is possible that in the future, these provers will be so smart that they can find and solve similar problems themselves, but currently this would not be useful either, in terms of money nor time, if the error can be corrected by a person after being found during the formal verification phase,” explains Veltri. 

Veltri’s work has two directions: the first is the theoretical development of new theorem provers aimed at the formal verification of software, which should have enough expressivity to reason with a large variety of programming languages. One way of thinking about theorem provers is as extremely smart notebooks. Users can type in mathematical expressions and prove theorems, whose correctness is assessed by the prover. Users can also interactively ask the system to prove some results for them, and the prover is often successful in this task. 

The other, more practical direction that the researcher is working on, is the use of these theorem provers for the purpose of formal verification of existing programming languages and the development of new languages. This task ensures the correctness of programs with respect to given specifications describing their intended behaviour. In turn, this allows for proactively improving and upgrading computer systems, guaranteeing their smooth functioning, which in today’s digital climate is crucial for many essential activities of everyday life. 

“It is difficult to explain, but the trend is in making software development simpler, more controllable and therefore ultimately, to improve it,” says Veltri. “Today, we are still in the process of creating theoretical solutions, but we have also put a little of it into practice. Although at a very low level at the moment, the initial results are rather promising.” 

Which field would benefit the most? 

In the long run, theorem provers could and should be used by all developers in the analysis of any program. At the moment, however, it can be seen that areas that require the most critical precision, as well as those where a lot of money is at stake, show the greatest interest in these formal methods. Veltri highlights self-driving cars and aviation, as well as insurance, banking and medicine as examples that would benefit with the use of theorem provers. 

“Let’s take a self-driving car. On the one hand, it requires an extremely large amount of information and on the other, a highly accurate, reliably faultless functioning system, from both its hardware and its software,” explains Veltri. “The correctness of self-driving car’s software can be assessed by testing the system millions of times, but it can only be truly assessed through formal verification. Surely, the highest guarantees of correctness is the fundamental goal we have for critical systems that are responsible for human lives, such as self-driving vehicles. Theorem provers figuratively act as “notaries”, certifying the correctness of the systems. They can also be used for finding bugs and subsequently improve the systems themselves.” 

When it comes to banking or medicine, where an incredible amount of secret, encrypted and restricted information travels, most of which also contains sensitive personal data, these systems must also operate in such a way that no handling errors occur. Most of the world’s major information leaks have been related to poorly-built systems, rather than hacking or malice. 

“It is interesting that many companies are increasingly creating units that deal with these issues. It is understandable that there is such a unit in Estonia, at companies such as Skype for instance, or Guardtime or Bolt, but banks and insurance agencies have also been affected by this development. Everyone is working so that these companies can be 100% certain that the software – or indeed, hardware – they develop or commission will function as it should. It is always a question of getting additional guarantees for both the organisation and their customers,” adds Veltri. 

The result is a safer digital society 

Veltri thinks that in 30 years, as a result of new high-assurance software and formal certification, our digital society will have reached a whole new level of security and reliability. But the question remains: what does the average person gain from all this? 

“It is computer program-based control of critical computer systems that are important to the state in the most fundamental aspects of modern life – online elections, banking, medicine – that restores the confidence in technology and science. Confidence which is currently rather shaky and low. This trust, in turn, provides us with a higher quality of life in every area of life,” he adds. 

Veltri notes that state-of-the-art technologies for software analysis and control are already in use in many successful IT companies around the world and in Estonia. In the coming decades, this phenomenon is expected to grow and expand, and it is also expected that the formal certification of programs will become standard procedure, and a central focus for every software company and state agency that creates computer systems. 

“As a result, the developers themselves, their customers and most importantly, the end users, will have the added reassurance that the programs that run our lives and use on a daily basis work correctly,” explains Veltri. 

The article was first published in the Estonian Centre of Excellence in ICT Research (EXCITE) magazine in 2021. 

Find out more about the EXCITE Center of Excellence: www.excite.it.ee

Photos: Hendrik Osula, Shutterstock

EXCITE is a project funded by the European Regional Development Fund.