Collaborative Research: FMitF: Track I: Reasoning About Shell Scripts and Their Effects in Context

Shell programming, the glue that holds modern computer systems together, is as prevalent as ever—steadily in the top 10 most popular programming languages in widespread use. It is also quite complex, due to the structure of shell programs, their use of opaque software components, and their complex interactions with the broader environment. As a result, even when exercising an abundance of care, shell developers discover devastating bugs in their programs during or after their execution—when it is too late to reverse any of their unintended effects. Bugs in these applications therefore affect—often with disastrous outcomes—engineers, scientists, and end-users alike: production bugs in industry platforms have resulted in the deletion of important user data. This project brings together a team of experts to develop fully automated, ahead-of-time program analysis techniques for checking the correctness of, and catching bugs in, shell programs before their execution. Drawing on techniques from programming languages, type systems, and program analysis, the project will benefit both developers and end-users to automatically catch and prevent undesirable or even catastrophic events. Of particular interest are the techniques proposed around the interaction of shell programs with the file system and the broader environment in which they execute. Beyond mere prevention, such techniques provide the foundations to precisely diagnose bugs and guide developers to implement effective fixes. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.