ソフトウェアの世界を切り拓く / Breaking Ground in the World of Software

松下 祐介 / Yusuke Matsushita

Published in 理学のススメ (An Encouragement of Science) No. 7 (PDF, HTML) in the University of Tokyo 理学部ニュース (News from Faculty of Science) Vol. 54, No. 1, May 2022. Originally in Japanese, Translated into English by the Author.

Our life is founded on various kinds of software. Apps of laptops and smart phones may come across your mind as software. Also, behind that, mouses, touch panels, graphics and networks are driven by another kind of software, too. Furthermore, home appliances around you, bank ATMs, cars and traffic lights in your city, MRIs in the hospital, airplanes and artificial satellites in the sky, they are all managed by some software.

Developing software is collaboration of humans and machines. Programmers design the computation for implementing the software they want and express that as a program in a programming language—the lingua franca between humans and machines. Of course, they try to avoid bugs—unintentional behaviors—by being careful and clever. But humans are not perfect. Too often, bugs slip in and get overlooked. One way to prevent that is to prove that the program satisfies the intended specification—verification.

In general, applications are built on top of many layers of abstractions. Among that, software of a low layer, near hardware, is called system software. It can achieve high-performance computation by operating directly on the memory. On the other hand, put under weaker protection, such software is more likely to have serious bugs.

I study software science, specifically how to verify system software.

In 2015, Rust was born as a programming language for developing robust system software. Now it has been rapidly and widely adopted in the industry. Rust has a strong static type system that automatically checks the memory safety of programs. Its key is ownership—access permission to a specific region of the memory. Types with ownership had long been academically studied, but Rust was the first to bring them into the mainstream, especially by introducing borrows, or temporary transfers of ownership.

型の保証を上手く使って、Rustプログラムを効率よく検証できないだろうか? Rustでは事前に期限を決めて所有権を借用できる。所有権があれば自由にメモリ上の値を更新できる。また、借用した所有権は分割でき、自由に捨てられる。そのあと、貸し手が所有権を回復したとき、更新後のメモリ上の値がわかるように、計算をモデル化すること。これが問題だった。
Can’t we verify Rust programs efficiently by using the guarantees of the types? In Rust, an object can borrow ownership by deciding the deadline beforehand. While having ownership, the borrower can freely update the values of the memory region. Also, borrowed ownership can be split and disposed of very freely. When the lender finally retrieves the ownership, we should be able to know the updated values of the memory region—the problem was how to build the model for that.

My lead-authored work RustHorn solved this by prophecy—peeking at values of the memory in the future ahead of time. The figure outlines the idea.

Overview of RustHorn

In our work RustHorn, we proved that this method provides an exact model to a wide class of Rust programs and also empirically demonstrated that it is useful for fully automated verification. Based on this work, a French student has been making a semi-automated verifier for Rust. My other lead-authored work RustHornBelt proved in the Coq proof assistant the correctness of RustHorn’s method for an even wider class of Rust programs. I am currently exploring a new approach to systems software development leveraging borrowing and prophecy.

Software development in the real world is very human, often requiring rough efforts. But for that reason, sharp ideas from science can be a spark to break new ground in the real world. Believing so, I do research again today.