Disclaimer: machine translated by DeepL which may contain errors.
~ Message from a graduate student~.
Pioneering the world of software
 |
| Yusuke Matsushita |
| Graduate School of Information Science and Technology, 2nd Year Doctoral Student |
| Birthplace Osaka |
| High School Nada Senior High School |
| Faculty Department of Information Science, Faculty of Science, The University of Tokyo |
Our daily life is supported by a lot of "software. First of all, do the various applications of personal computers and smartphones come to mind? It is also software that operates the mouse, touch panel, graphics, and network behind the scenes. Software also controls the home appliances around us, ATMs in banks, automobiles running in the streets, traffic lights, MRIs in hospitals, airplanes, satellites, and so on.
Software development is a collaborative effort between man and machine. Programmers express specific calculation methods to realize the desired software as programs in a programming language, i.e., a language common to humans and machines. Of course, they develop software with care and ingenuity to avoid unintended behavior, the so-called "bugs. Even so, because this is a human task, bugs are often created and overlooked. One method to prevent this is verification, which logically proves that the program meets the intended specifications.
In general, an application is obtained by layering several layers of abstraction, of which the software at the lowest layer, close to the hardware, is called "system software. In particular, it can achieve high-performance computation by directly manipulating memory. On the other hand, such software is not well protected by error detection, so there is a high risk of serious bugs being embedded in it.
I study software science, especially verification of system software.
In 2015, the language "Rust" was born and is rapidly being used in industry as a language for developing robust system software. The key to this is "ownership," the right to access specific areas of memory. Ownership-based types have been studied for a long time, but Rust takes them to a practical level by introducing a mechanism called "borrowing," in which ownership is temporarily passed on.
Can't we use type guarantees to efficiently verify Rust programs? Rust allows borrowing of ownership for a predetermined period of time. With ownership, we can freely update values in memory. The borrowed ownership can be divided and discarded at will. Then, when the lender restores ownership, model the computation in such a way that the updated value in memory is known. This was the problem.
My lead paper, "RustHorn," solved this with the idea of "prophecy," which anticipates future values in memory. The figure below shows the outline.
Example of verification by RustHorn
RustHorn proved that the method can rigorously model a variety of Rust programs and experimentally demonstrated its usefulness for automatic verification. As an influence of this research, a full-scale semi-automatic Rust verifier based on this method has been built by a French student. In my other main paper, "RustHornBelt," I proved the validity of RustHorn's method for a wide class of Rust programs with a proof support system called Coq. I am now exploring a new form of systems software development using borrowing and prophecy.
The actual software development is a very human activity, and sometimes it is very muddy. That is why sharp ideas of science can be the light that opens up the field. With this belief, I continue my research today.