Automatic Verification of MIR Optimizations in the Rust Compiler; Nonmedical Vaccine Exemptions: A Balance of Rights

Whitaker, Nathan, School of Engineering and Applied Science, University of Virginia
Martin, Worthy, EN-Comp Science Dept, University of Virginia
Baritaud, Catherine, EN-Engineering and Society, University of Virginia

Each day, we rely on massive, complex sociotechnical systems to keep us safe and secure. In computer systems, a vast network of unseen components lies beneath the technology we use, and the operation of these hidden parts can ensure, or threaten, the security of the system. The technical research focuses on securing the software which takes part in the creation of almost all computer programs, so that the entire system can benefit despite the limited scope of the solution. Similarly, public health relies on the cooperation on of countless moving parts, including all members of society. In order to counter the rise of preventable disease, the science, technology, and society (STS) research focuses on examining and remedying local and state-level loopholes that allow individuals to avoid vaccination and endanger herd immunity. By identifying and applying localized measures that have a large impact on the systems around us, measurable, incrementable improvements can be made to the issues facing society.

Computer systems have rapidly become critical to society, but cybersecurity has struggled to keep up with this pace. As computer systems grow in size, it becomes increasingly challenging to secure them. There is one piece, however, that touches almost all software. Compilers are programs that translate source code into a format that computers can run, and produce the vast majority of software. The technical research focuses on creating a tool to automatically verify the correctness of processing performed by a compiler, in order to improve the security and soundness of software as a whole.

The technical research laid out the design for a piece of software which verifies that a compiler has correctly preserved the intended behavior of a program. The tool operates automatically and is easily integrated into existing systems. This ease of use is crucial because it increases the rate of adoption and enhances the real-world usefulness of the research. In detailing this design, the research has successfully provided the foundation for the implementation and integration of the tool into real-world applications. Once implemented, this would secure the foundation of the complex computer systems that are increasingly central to modern life.

In a disturbing trend, vaccination rates have been falling recently, despite vaccine mandates in all states, and the incidence of preventable disease has risen. One aspect contributing to falling vaccination rates is the increasing number of nonmedical exemptions to vaccine mandates. The STS research focused on determining whether or not nonmedical vaccine exemptions are a moral right, and how the exemption system may be reformed to increase vaccine adoption. Actor Network Theory was used as the framework for the analysis of the interactions surrounding nonmedical vaccine exemptions. The analysis drew upon academic research, ethical readings, and real-world communications from stakeholders to assess the situation and evaluate possible solutions to the rise in vaccination mandate exemptions.

The STS research asserts that there is no moral or ethical right to be exempt from vaccine mandates for nonmedical reasons. Vaccine refusal is not a matter of simple individual freedom, as it forces others to shoulder the burden of individual decisions, and infringes on the safety of society as a whole. There is therefore no moral right for nonmedical exemptions to be permitted. Due to the resistance of vaccine hesitant groups, religious organizations, and legislatures, the elimination of nonmedical exemptions is not the ideal solution for the immediate future. Instead, efforts should focus on introducing barriers to nonmedical exemptions, such as requiring vaccine education classes for individuals seeking exemption, as well as connecting with local communities to improve trust in vaccination.

Despite the challenge of addressing widespread problems within complex systems, large-scale improvements can be achieved through the careful identification of high-impact local measures. Whether it be the security computer systems or public health, real progress can be made by focusing on concrete, achievable problems around us.

BS (Bachelor of Science)
Actor Network Theory, Compiler, Verification, Rust, Vaccination, Public health policy

School of Engineering and Applied Science
Bachelor of Science in Computer Science
Technical Advisor: Worthy Martin
STS Advisor: Catherine Baritaud
Technical Team Members: Nathan Whitaker

All rights reserved (no additional license for public reuse)
Issued Date: