|
Could We have Saved the Death Star Jose Meseguer
The branch of software engineering called formal methods is vital as our systems become increasingly large and complex and we rely upon them more, especially for applications in which the cost of failure is death or considered to be very high. Had Darth Vader employed formal methods to the design of his Death Star, perhaps it would not have been vulnerable to the starfighter attack that led to its destruction. The same could be said for the security holes in the Windows OS that make it a frequent target for hackers. What if someone could hack into the flight control system of a plane via the onboard entertainment system? What about other complex systems? How can we guarantee their reliability? How do we make these systems secure without sacrificing interoperability and ease of use? These are some of the questions that researchers at Illinois are answering using formal methods.  Grigore
RosuThe Department of Computer Science at Illinois has perhaps the strongest team of formal methods researchers in the country, comprising eight experts in the field: senior faculty members Gul Agha, Carlos Gunter, Elsa Gunter, and Jose Meseguer, and rising stars Darko Marinov, Madhu Parthasarathy, Grigore Rosu, and Mahesh Viswanathan. Formal methods is a major thrust of the Information Trust Institute (ITI), the nation's leading research and education center devoted to trustworthy and secure information systems. Based at Illinois, about half of ITI's researchers are from the computer science department. Additionally, the mathematics department at Illinois boasts one of the country's strongest groups in mathematical logic, the underpinning of formal methods. The opportunities for powerful collaborations are exciting and abundant. "They are all excellent people," said Meseguer, referring to talent pool at Illinois. "We can all do things individually, but together we can make a bigger impact by embarking on longer term, challenge problems. We can show that difficult problems can be solved by combining our technical strengths in a more ambitious way." Formal methods are mathematically based techniques for the specification, development, and verification of software and hardware systems. The notion of formal methods has been around for more than 50 years, but because computers have recently become pervasive in safety-, security-, and mission-critical systems, the field is now enjoying resurgence and garnering some media buzz. In 2002, Bill Gates pointed out Microsoft's use of formal methods, saying that "things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example driver verification, we're building tools that can do actual proof about the software and how it works in order to guarantee the reliability." Intel used formal methods to prove the reliability of parts of the Pentium 4 and Itanium chips. Most recently Green Hills Software announced their use of formal systems in the specifications of their latest OS security policy and architecture. In traditional software engineering, designers attempt to prove that a system will be reliable and secure by exhaustive testing, probability theory, and simulation. No one would argue that it is better to develop software with no bugs than to write it with lots of bugs and spend lots of time getting rid of them, but in the rush to get a product out the door, buggy software has become a fact of life. Formal methods can help, but they have a long way to go before they are universally adopted by industry as de rigueur in the design process, partly because it is not well understood and because there are not enough practitioners in field. In fact, Microsoft issued a request for proposals last year to introduce formal methods into the undergraduate computer science curriculum Computer science Professors Jose Meseguer and Grigore Rosu work on the frontier of formal methods research and understand the futility of using traditional testing methods for large and complex systems. "People have very few ways to understand how systems work," said Meseguer. "They may have some drawings, or some text, and so forth, but until they actually build the system, they won't know what will happen. It is when you test the system that you discover all kinds of problems, and by that time, it is often too late. They have to scramble around to make it work because they already have too much invested in the project. Plus there may be more combinations and permutations of conditions than there are atoms in the universe." Rosu agreed, saying "testing never proves correctness. You have a higher degree of confidence the more you test, but you can never test everything. For instance, you could never test al the different programs that will be run on a particular system." On the other hand, applying formal methods during the design phase gives designers both analytic and predictive power and can prevent system designers from proceeding down a path that ultimately won't work. One of Rosu's current projects is Runtime Verification and Monitoring. The idea is to check the properties of a program while it is running. If specifications are violated, the system is recovered at runtime. This avoids the difficult task of having to prove all possible behaviors by looking only at the behavior that is taking place. Rosu explained: "We run the program and observe it. We know what properties to check against, so we check them at runtime and observe and monitor them. If we detect a problem, we recover and fix it. Then we can guarantee that part. There may still be a bad combination somewhere, but it is so unlikely to happen that we don't worry about it." Not only can this method detect errors in concurrent programs, but is also scales well and can be performed online. Special versions of Runtime Verification and Monitoring have been used by NASA to find bugs in their software. Another related project is Domain-specific Certification of Software. In this approach a program is checked against one particular aspect to make sure it is error free by using certifiers. The certifiers only check a program for those aspects and generate proofs of correctness that count as a certificate. This certificate can be independently checked, both dynamically and statically, by other people. Meseguer is currently working in the area of Formal Executable Specifications, an idea based on mathematical models. These models are collections of mathematical axioms- fundamental assumptions or formulas that are universally valid. The question is, can you make these axioms executable so that in fact they are a high-level program that models or simulates an intended system before it is built? After all, a computer program is a formal specification that tells the computer what to do, and a programming language is a formally defined language with precise semantics. To answer this question, Meseguer has developed a language called Maude. Maude is a rewriting engine used to write, execute, and analyze executable models of the logic of complex systems. Rosu is also involved in the design and implementation of programming languages. "We need better programming languages," he said. "The ones we have now allow programmers to do too many crazy things." His approach is to use a universal model based on term rewriting, in which structures keep transforming according to certain rules so that you have patterns transforming into other patterns. The idea is to find places where these patterns match. As terms keep evolving, the result is a very simple computation model with full computability power. Complex algorithms can be defined with rewrite rules. "Anything that can be computed can be computed this way," said Rosu, giving a simple example of computing 100! (100 factorial). Normally, this is achieved in a conventional programming language by establishing a loop that runs sequentially to compute the answer. Using the universal model approach, this can be computed simply by establishing two general rules of transformation: 1!?1 and n! ?n?(n-1)! Starting with n=100, each time a subsequent number for n is plugged in, the result is a pattern (for instance a tree structure) that has been transformed from the last one. As patterns or parts of patterns match each other, the program will keep making transformations and progress until the final answer is reached. "It's an interesting and human model of computation," Rosu continued. "The nice thing about it is that it supports concurrency naturally. Many earlier languages were designed to be sequential. By rewriting, you can rewrite these rules concurrently. We have to do something special to make it sequential. The future is all about concurrency, and the future of programming languages will be concurrent. Rewriting itself is powerful enough to be a language." But he admits that it is hard to change peoples' favorite programming languages. Right now, only researchers are using rewriting engines like Maude. Rosu pointed out that Europe has more activity in formal methods research than the U.S. The hope is that as students here are educated about formal methods, they will bring it with them into the mainstream. Written by Judy Tolliver, May 12, 2005
|
|