Mentors: Chris Timperley and Claire Le Goues

Description and Significance
As robots are becoming increasingly safety-critical and complex, a large amount of software engineering research has been addressing the challenges of architecting, constructing, and maintaining robotics systems. However, most of this research has been conducted on only a small number of systems. In this project we want to increase the scope to all robot software projects on GitHub written for the Robot Operating System (ROS), the most popular framework for robotics systems. We will try to find real-world bugs, and get a deeper understanding of the software architecture of robotics systems, meaning how they are composed and how they evolve.

Student Involvement
The student on this project will learn how to analyze a large amount of software repositories and apply these skills by conducting a large-scale analysis of the architecture of open-source ROS-based robotics systems, including their composition, evolution, and potential bugs. The student will build on our existing robot software analysis tools to study how robot architectures evolve over time, what kinds of bugs are introduced, and how they are addressed.

References
ROSDiscover: Statically Detecting Run-Time Architecture Misconfigurations in Robotics Systems. Chris Timperley, Tobias Dürschmid, Bradley Schmerl, David Garlan, and Claire Le Goues. ICSA 2022. https://doi.org/10.1109/ICSA53651.2022.00019

It takes a village to build a robot: An empirical study of the ROS ecosystem.
Sophia Kolak, Afsoon Afzal, Claire Le Goues, Michael Hilton, Christopher Timperley . ICSME 2020. https://par.nsf.gov/servlets/purl/10210655

Mentors: Jonathan Aldrich

Description and Significance
Diagrams are a vital educational and explanatory tool; there does not exist an area of study which does not make extensive use of them. As a result, much research has been done into computer programs which generate diagrams [1, 2], affording innumerable people and fields easy access to advanced visualization capabilities.

Areas in which current diagramming capabilities are lacking are modularity, compositionality, and abstraction. This makes questions like "Which diagrams can I sensibly put together to make a new diagram?" and "Which diagrams can I transform this diagram into?" difficult to answer. Many existing solutions are ad-hoc.

This project aims to provide type-driven answers to these elusive aspects of diagramming. Specifically, by providing a type theory specialized to concerns typically encountered while manipulating visualizations, we hope to bring the benefits enjoyed by programming languages to visualizations.

Student Involvement
A student involved in this project could tackle this problem from a number of directions. For the more theoretically-inclined, this could involve designing a type system for diagrams from first principles, and possibly exploring its formal properties. For those with more experience or focus in implementation, the same project could be confronted in an experimental way, by seeing what works in a prototype diagramming tool. A user study for investigating common issues with diagramming tools is also a possibility. This project is best suited to students with some prior exposure to type systems, but this can also be taught as part of the project and is not a requirement.

References
[1] https://penrose.cs.cmu.edu/

[2] https://vis.csail.mit.edu/

Mentors: Joshua Sunshine and Brad Myers

Description and Significance
Generating a robust test suite is often considered one of the most difficult tasks in software engineering. In the United States alone, software testing labor is estimated to cost at least $48 billion USD per year. Despite high cost and widespread automation in test execution and other areas of software engineering, test suites continue to be created manually by software engineers. Automatic Test sUite Generation (ATUG) tools have shown promising results in non-human experiments, but they are not widely adopted in industry.

Prior research provides clues that traditional ATUG tools may not be well-aligned to the process human software engineers use to generate test suites. For instance, some tools generate incorrect or hard-to-understand test suites while others obscure important information that would help the software engineer evaluate the quality of the test suite. Often these problems are evident only by observing software engineers using these tools.

NaNofuzz was recently featured on the Hacker News homepage. Lean more about NaNofuzz at its GitHub repository here: https://github.com/nanofuzz/nanofuzz

Student Involvement
This research initiative will flex your research muscles: you will approach the problem of test suite generation using a comprehensive mix of theory, human observation, PL, HCI, and prototype engineering. You will gain insights using our emerging theory of test suite generation to and using innovative prototype tools, such as NaNofuzz, that you help build. This comprehensive approach will expand your research skill set and help you discover new science-based solutions that may make testing easier and more enjoyable for the 26+ million (estimated) software engineers on earth today.

Mentor: Alessandro Acquisti

Description and Significance
The Privacy Economics Experiments Lab (PeeX) at the Heinz College at Carnegie Mellon University (CMU) has been developing a complex and ambitious infrastructure to conduct a study on the impact of adblock and anti-tracking technologies on users’ behaviors. The study consists in a large-scale field experiment, involving over 1,000 participants, and will focus on how installing ad-blocking and/or anti-tracking tools affects online browsing and purchasing behavior. The experiment relies on a complex client-server infrastructure (including a Chrome extension and a Thunderbird plugin, and servers hosted at CMU) developed by Professors Alessandro Acquisti at CMU and Cristobal Cheyre at Cornell with the help of several graduate, undergraduate, and prior REUSE students. The experiment will start collecting data in January 2024. During the summer of 2024, we expect to engage in in-depth data analytics exercises, focused on investigating the vast amount of browsing and other online behaviors that the experiment will generate.

Student Involvement
There are many ways to get involved in this project. One of the primary goals during the summer will be data analytics. Therefore we can expect summer students to be involved in tasks such as:

1. Writing scripts to extract and process data collected during the experiment
2. Analyzing data using a variety of techniques and methods
3. Interacting with experimental participants
4. Monitor study participants’ compliance with experimental conditions

Experience with SQL, Python, and JavaScript are nice-to-have. Knowledge of, or willingness to learn, data analysis and statistical packages is important. 

References
Frik, Alisa, Amelia Haviland, and Alessandro Acquisti. "The Impact of Ad-Blockers on Product Search and Purchase Behavior: A Lab Experiment." 29th USENIX Security Symposium (USENIX Security 20). 2020.

Mentor: Travis Breaux

Description and Significance
Software requirements describe the normative behaviors that users and other stakeholders come to expect from the systems they use. Government laws, regulations and policies increasingly overlap with software requirements, especially as software is key component in the realization of process automation and artificial intelligence. How we guide companies in the design and development of products and services that respect human and societal values, such as safety and privacy, is a key challenge.

In this project, we aim to address this challenge by combining techniques from psychology, logic and natural language processing to build models that learn whether systems satisfy legal and policy requirements, while enabling design space exploration, when systems are poorly described or when they exhibit behaviors that conflict with requirements. This project combines theory about human language understanding and legal reasoning with advanced prompt engineering techniques using large language models. Students will learn about state-of-the-art prompting strategies and applications, including Chain-of-Thought reasoning (Kojima et al., 2022) and ontology construction (Wei et al., 2023). Students will also participate in the design of experimental pipelines to train, generate and evaluate dialogic systems (Ouyang et al., 2022) for the analysis and validation of software requirements.

References
Kojima et al., “Large Language Models are Zero-Shot Reasoners.” (NeurIPS 2022)

Ouyang et al. “Training language models to follow instructions with human feedback,” (NeurIPS 2022)

Wu et al., “Do PLMs Know and Understand Ontological Knowledge?” (ACL 2023)

Mentor: Joshua Sunshine

Description and Significance
Visual aids play a critical role in communicating ideas in STEM fields. Having high-quality, easy-to-understand visualizations of a concept can be the difference-maker in one’s understanding. Adding interactivity as a medium for storytelling, whether through animation or otherwise, further empowers students to explore alternatives, break multi-part processes into digestible pieces, gain instant feedback on their actions, and deepen their conceptual understanding. However, existing tools to build visual aids are often time-consuming to use and require specialized knowledge such as coding, animation, or design. We want to minimize the effort and expertise required to create beautiful, high-quality visual aids.

In this project, we aim to develop a tool that allows users to create sets of diagrams that show transitions between stages, for instance, illustrating the steps in a geometric proof or the changes in molecular structure during a chemical reaction. In order to make this possible, we need to develop a quantifiable way to evaluate the "goodness" (i.e. ease of processing for a viewer, minimized design distractions, maintained visual consistency between stages, etc.). This will involve running a human subjects study to observe how people process staged diagrams.

Student Involvement
There are many options to get involved in this project! We are looking for students who are interested in working at the intersection of HCI, design, and software engineering. There are opportunities to get involved with user studies, designing delightful user experiences of software, and plenty of technical challenges that arise from automating layout of diagrams and creating usable tools for end-users. 

Mentors: Chris Timperley and Claire Le Goues

Description and Significance
Due to the increasing integration of robots into our lives and work environments, bugs in robotics systems are especially dangerous. One way to identify tricky-to-find bugs in complex, safety-critical systems is via model-based analysis. However, creating analyzable models for hundreds of software components manually is often a tedious, labor-intensive, and error-prone process. Instead, we created a technique to automatically infer formal models from code for systems implemented for the Robot Operating System (ROS), the most popular framework for robotics systems, using a combination of static and dynamic analysis by exploiting assumptions about the usage of the ROS framework. This work is a contribution towards making well-proven and powerful but infrequently used methods of model-based analysis more accessible and economical in practice to make robotics systems more reliable and safe. We plan to make this tool more accessible to practitioners and increase the practical impact of this work.

Student Involvement
The student on this project will learn how to build usable and practical tools for automated bug finding in C++ and Python and apply these skills by extending our tool to work for typical development workflows and support the newer version of ROS.

References
ROSDiscover: Statically Detecting Run-Time Architecture Misconfigurations in Robotics Systems. Chris Timperley, Tobias Dürschmid, Bradley Schmerl, David Garlan, and Claire Le Goues. ICSA 2022. https://doi.org/10.1109/ICSA53651.2022.00019

Mentor: Eunsuk Kang

Description and Significance
Network protocols play an important role in our computer systems by providing ways for different machines to securely and reliably communicate to each other. Most protocols are deployed with certain assumptions about how the underlying network behaves (e.g., it does not lose or duplicate messages). In practice, however, some of these assumptions may be violated due to unexpected faults and possibly undermine the correctness of a protocol that relies on it. The goal of this project is to develop rigorous and automated methods for designing protocols that are robust, in that they are capable of ensuring critical properties even under the presence of possible disturbances in the underlying network.

Student Involvement
The student will be using formal modeling tools (such as TLA+ and Alloy) to specify protocols and develop new analysis methods that can be used to evaluate the robustness of a protocol against a misbehaving environment. They will gain experience using the state-of-the-art specification and verification tools, and also learn about computer networking and distributed systems.

Mentor: Haiyi Zhu

Description and Significance
The gig economy is characterized by short-term contract work performed by independent workers who are paid in return for the "gigs" they perform. Example gig platforms include Uber, Lyft, Postmates, Instacart, UpWork, and TaskRabbit. Gig economy platforms bring about more job opportunities, lower barriers to entry, and improve worker flexibility. However, growing evidence suggests that worker wellbeing and systematic biases on the gig economy platforms have become significant societal problems. For example most gig workers lack financial stability, have low earning efficiency and lack autonomy, and many have health issues due to long work hours and limited flexibility. Additionally, gig economy platforms perpetuate biases against already vulnerable populations in society. To address these problems, this project aims to build a community-centered, meta-platform to provide decision support and data sharing for gig workers and policymakers, in order to develop a more vibrant, healthy, and equitable gig economy.

Our prior interview and workshop studies suggest that policymakers must provide more targeted, personalized, and democratized policies, benefits, and protections for platform-based workers. Our most recent work revealed that government agencies and workers lack data on existing gig work conditions to make informed decisions. Specifically, we found that policy domain experts expressed keen interest in data for advancing policy on a number of initiatives, including equity, fair pay, and worker safety. While gig workers share concerns about similar issues, they also pine to leverage aggregate-level data to improve earnings as well as exchange experiences and strategies.

In order to improve gig work conditions, we hypothesize that a co-designed data-exchange platform can advance policies for improving gig work well-being, empowering gig workers, and bridging the gap between government agencies and gig workers. Given that the existing gig economy platforms do not have the incentives to share their data, we propose to develop a worker-controlled “data exchange” platform to address the data challenges of policymakers and gig workers. We will work closely with gig workers and our municipal, nonprofit, and labor union partners in Allegheny County, to co-create a system that allows workers to contribute a variety of data related to gigs and enable data- and experience-sharing in a responsible, ethical, and privacy-preserving manner. The data exchange platform will allow gig workers to contribute quantitative data (e.g., working hours, payment histories) as well as qualitative experiences (e.g., strategies, narratives), so as to enable aggregate-level sharing and analysis of wage patterns and successful strategies. The collected data will enable workers to (1) compare wages across gigs and platforms (2) reverse engineer instances to algorithmically determined pay changes (e.g., commission surges), and (3) record shared experiences and build a collective worker community.

Mentor: Chris Timperley

Description and Significance
Robotics has been increasingly entering the public domain, most notably in the form of self-driving cars. This increase in public exposure comes with a corresponding increase in public risk. A recent string of accidents in the self-driving car space has made it apparent that these systems are not yet safe enough for this level of operation in the public space. In this project, we aim to apply robotics robustness testing tools to an open source self-driving car system, to measure its ability to safely handle off-nominal conditions, and evaluate the risk this system poses to those around it.

Student Involvement
The REU student involved in this project will set up open source self-driving software and integrate robustness testing tools. The student will learn about robustness testing techniques in the robotics space, and contribute to open source robustness testing code. The student will learn how to spin up off-the-shelf robotics systems and how to write test scenarios and test oracles to identify unsafe behavior in these systems.

Mentor: Fei Fang

Description and Significance
As we push the boundaries of how machines learn and make decisions, it is crucial to ensure we fully understand the processes involved. Influence functions have been a key to clarifying complex algorithms in machine learning [1]. Our envisioned new project takes this understanding further by applying these functions specifically to offline reinforcement learning (RL), where we want to attribute the decisions made by the policy to certain trajectories the agent has encountered during its offline training. If we can translate the decision-making of offline RL into something we can better interpret, we would be able to build better policies that we can trust and use responsibly, which is especially important when these systems are used in critical areas that affect our daily lives.

Student Involvement
The student will be leading this project, with detailed guidance and feedback from the faculty advisor and a Ph.D. student. The student will engage in an end-to-end research process from exploratory literature reviews to the practical implementation of the developed methods and paper writing. We are looking for students with a foundational knowledge of machine learning and an interest in (or experience with) offline reinforcement learning, as well as the curiosity and drive to learn.

References
[1] Koh, Pang Wei, and Percy Liang. "Understanding black-box predictions via influence functions." International conference on machine learning. PMLR, 2017. [2] Deshmukh, Shripad Vilasrao, et al. "Explaining RL Decisions with Trajectories." arXiv preprint arXiv:2305.04073 (2023).

Mentor: Rohan Padhye

Description and Significance
Date and Time are some of the most fundamental concepts on which many systems rely. Getting date/time computations wrong can lead to critical system failure, expose security vulnerabilities, or lead to hard-to-detect race conditions. Most programming languages have date/time utilities in their standard libraries, or there are popular packages that provide such functionality. But, date and time computations are subtly difficult to implement correctly because of the variety of complexities associated with things like time zones, daylight savings, leap years/seconds, ambiguous date formats, local vs. absolute time, arithmetic between date/time values, and mixing of reference systems such as UTC and atomic time, and much more! In this project, we aim to devise ways to rigorously test and validate date/time libraries in languages such as Python and Java, as well as provide tool support to assist developers using these libraries.

Student Involvement
Students working in this project will get familiar with various complexities with date/time computations and first do an empirical study of date/time related bugs from open-source issues on GitHub. Students will then work with property-based testing libraries like Hypothesis or fuzzing tools like JQF to devise logical consistency properties that date/time computations must satisfy across various APIs and perhaps even across programming language boundaries. As a stretch goal, students can leverage LLMs such as GPT-4 to validate date/time implementations with respect to natural language specifications given in RFC documents.

Students are expected to have a strong background in programming in Python or Java, be familiar with GitHub and open-source processes, and have a general interest in software quality and/or security. Experience with operating systems code or programming languages / compilers is a bonus.

Mentor: Claire Le Goues

Description and Significance
About $100 billion has been invested in self driving car development. After all of that, and many recent high profile failures, we're confident that they are difficult to develop. Now it is your turn to discover failures in machine-learning based self driving car algorithms.

In this project, we will develop new methods for quickly finding failures by testing self driving car algorithms in simulation. We'll build on a varied set of technologies including differentiable rendering, adversarial algorithms, testing environment generation, and deep learning. We will develop a testing system that creates an initial scene for a self driving car algorithm, then makes modifications such as moving a traffic cone or changing the lighting, until the algorithm demonstrates unsafe behavior. Uniquely, we plan to encode those changes in a differentiable way, so we can use gradient descent to find those catastrophic changes quickly.

We're looking for a student with experience in Python who ideally has some exposure to calculus and linear algebra. If you have experience in any graphics, machine learning, robotics, or game development, you're an especially good fit. If you don't have experience with all or even any of those, but you have interest, this project may be a great place to learn, and we're happy to teach you.

Student Involvement
The student on this project will learn how to build usable and practical tools for automated, self driving car bug finding in Python and apply these skills by extending our existing work on adversarial grasping to work for self driving car algorithms.

Mentors: Mayank Goel and Jill Lehman

Description and Significance
Increased access to modern surgical health care goes hand-in-hand with the need for post-operative self-care. Patients tend to perform self-care alone and are typically uncertain, untrained, fatigued, and shouldering significant additional responsibilities. The problem is compounded further by low levels of health literacy. To support patient self-care, we are developing an AI-driven agent that uses multimodal activity and behavior sensing – movement, sound, and patient’s own self-narration of their actions – on a commercial watch to provide situated and context-aware voice-based guidance. Our goals are to advance aspects of at-home healthcare and, more generally, contribute to basic science in adaptive, real-time, in situ multimodal interactions. Over the past two years we have worked with Dr. Bryan Carrol to collect patient data with early versions of the technology in the context of post-operative wound care for Mohs Micrographic Surgery, a technique of surgical excision applied to skin cancers on the head and neck.

Student Involvement
The student will be building on initial work with the self-narration data that uses foundation models like GPT to explore whether and under what circumstances such models can answer patient’s questions. Working closely with other project members, the student will need to learn the existing pipeline for testing, and become familiar with the existing results from different foundation models (e.g., open source vs not) and multiple contexts and prompts, with a particular focus on analyzing error and edge cases. Once familiar, the student’s main activity will be to extend the pipeline to use foundation models to automatically track linguistic indicators of where the patient is in the procedure, and apply it in an analysis of at-home vs in-clinic data. We are looking for students with background in linguistics or NLP, Python programming, and practical experience with APIs for LLMs. Prior experience in prompt hacking, Retrieval-augmented generation (RAG) and/or use of knowledge graphs particularly welcome.

Mentor: Jonathan Aldrich

Description and Significance
SASyLF is a proof assistant designed to help students learn about proofs in programming languages, such as type soundness. Internally, the tool is based on the Edinburgh Logical Framework, but students are able to write proofs in a notation that closely resembles the "blackboard notation" used in programming language courses. Therefore, students are able to get immediate feedback on the correctness of their proofs, but need not confront the steep learning curve of the "industrial strength" tools used in research papers.

Student Involvement
In a course offered this year at CMU, we observed several areas for improvement in SASyLF. The REU student will learn about SASyLF and some of the internal technologies it uses, such as higher-order pattern unification. They will adapt a recently developed algorithm that is complete for the pattern fragment of higher order unification problems to the setting of SASyLF, supporting greater expressiveness and better error reporting. Some prior background in theorem provers or type theory is helpful.

References
www.sasylf.org

SASyLF: An Educational Proof Assistant for Language Theory. Jonathan Aldrich, Robert J. Simmons, and Key Shin. In Proceedings of Functional and Declarative Programming in Education (FDPE '08), 2008. http://www.cs.cmu.edu/~aldrich/SASyLF/fdpe08.pdf

Mentor: Hanan Hibshi

Description and Significance
The expansion of blockchain into different applications is increasing. When more lines of code are introduced in any software application, the attack surface increases because new lines of code could open the door to more software bugs/vulnerabilities. After all, software developers approach blockchain technology as programmable software where they get to use software tools that are more specific to developing blockchain applications.

We continue to see vulnerabilities in software on the rise year after year. Almost every application on the market has a vulnerability reported with a recorded CVE number(s). We envision blockchain software to be no different as programmers may continue to make mistakes that introduce software bugs/vulnerabilities. In this proposal, our goal is to study how common vulnerabilities (e.g., integer overflow) may exist in code written for the blockchain. This work will generate examples of code that contains such vulnerabilities and make these available for future testing and educational purposes with and for blockchain developers.

Student Involvement
The student will be will be learning about smart contracts code and compiling a set of examples of blockchain code that contains common software vulnerabilities with recommendations on how to avoid/fix these vulnerabilities in code. Student will be creating tutorials for smart contract beginners that guide them through these vulnerabilities using the code examples they developed.

Mentors: Ben Titzer and Heather Miller

Description and Significance
Engineering a resilient distributed system is difficult due to the complexities of partial failure. One promising approach to improve resilience is fault injection testing, but all tools to-date are either manually configured or are tied to a specific programming language. Wasm, as a bytecode that runs on a virtual machine, provides a portable, universal platform for distributed systems that has the potential for great developer tooling since it is a compilation target for many programming languages and supports important debugging functionality. We are building a tool that automatically injects faults into distributed systems during local testing by compiling the distributed system components to Wasm and instrumenting the bytecode. Thus far, we have successfully injected faults into nodes running on Dfinity’s Internet Computer platform and we hope to reach a new domain in this project!

Student Involvement
If you’re interested in research that builds developer tooling to make distributed systems more fault tolerant, you should apply! Students working on this project will extend and leverage our tool to inject faults in a new context: microservices. Students will gain knowledge in many different domains such as bytecode instrumentation, resilience engineering, and microservices. They will also gain skills in working with several different languages like Rust, Virgil, a new DSL specifically for instrumentation (similar to dtrace’s D language), and even Wasm bytecode!

Mentor: Fei Fang

Description and Significance
In the face of rising cyber threats and evolving attacks, adaptive defense strategies are essential. Deception, using honeypots as bait for malicious actors like hackers, stands out as a promising tactic to hinder attackers and drain their resources. Our prior work introduced the Adaptive Cyber Deception Game, a two-player Markov game model that considers sequential interactions between defenders and attackers in cyber deception scenarios. This model forms the basis for practical defense strategies in real enterprise networks. Initial assessments using reinforcement learning (RL) techniques have shown that RL-based strategies outperform heuristics in abstract game simulations. Our future plans involve refining the model to mirror real-world cyber deception scenarios and developing multi-agent RL algorithms to compute and evaluate defender strategies in emulated networks on cloud platforms like AWS.

Student Involvement
As a student, you will collaborate closely with a PhD student, working under the guidance of our faculty. Your initial tasks will involve assisting the PhD student in abstracting a real-world scenario and formulating it as a game aligned with our developed game model. Subsequently, you will take the lead in creating an emulated network that replicates this scenario and ensures its functionality on cloud platforms like AWS. By participating in this project, you will gain experience in cyber security and Artificial Intelligence (more specifically, game theory and multi-agent RL), and you may even have the opportunity to engage with ethical hackers who will simulate attacks on the emulated network, providing a practical assessment of our defense strategies. Interests or experience in cybersecurity are needed. Familiarity with AWS/OpenStack is a plus but not required.

References
Fang, F. (2021). Game Theoretic Models for Cyber Deception. In Proceedings of the 8th ACM Workshop on Moving Target Defense (pp. 23–24). Association for Computing Machinery. https://doi.org/10.1145/3474370.3485656

Li, L., Fayad, R., & Taylor, A. (2021). CyGIL: A Cyber Gym for Training Autonomous Agents over Emulated Network Systems. arXiv:2109.03331 [Cs]. http://arxiv.org/abs/2109.03331

Schulman, J., Wolski, F., Dhariwal, P., Radford, A., & Klimov, O. (2017). Proximal Policy Optimization Algorithms (arXiv:1707.06347). arXiv. https://doi.org/10.48550/arXiv.1707.06347

Du, Y., Song, Z., Milani, S., Gonzales, C., & Fang, F. (2022). Learning to Play an Adaptive Cyber Deception Game. The 13th Workshop on Optimization and Learning in Multiagent Systems, AAMAS, 2022.

Mentor: Christian Kästner

Description and Significance
The advances in machine learning (ML) have stimulated widespread interest in integrating AI capabilities into various software products and services. Therefore today’s software development team often have both data scientists and software engineers, but they tend to have different roles. In an ML pipeline, there are in general two phases: an exploratory phase and a production phase. Data scientists commonly work in the exploratory phase to train an off-line ML model (often in computational notebooks) and then deliver it to software engineers who work in the production phase to integrate the model into the production codebase. However, data scientists tend to focus on improving ML algorithms to have better prediction results, often without thinking enough about the production environment; software engineers therefore sometimes need to redo some of the exploratory work in order to integrate it into production code successfully. In this project, we want to analyze collaboration between data scientists and software engineers, at technical and social levels, in open source and in industry.

Student Involvement
We want to study how data scientists and software engineers collaborate. To this end, we will identify open source projects that use machine learning for production systems (e.g., Ubuntu's face recognition login) and study public artifacts or we will interview participants in production ML projects. This research involves interviews and analysis of software artifacts. We may also develop exploratory tools to define and document expectations and tests at the interface between different roles in a project. The project can be tailored to the students’ interests, but interests or a background in empirical methods would be useful. Familiarity with machine learning is a plus but not required. Note, this is not a data science/AI project, but a project on understanding *software engineering* practices relevant to data scientists.

Mentor: Jonathan Aldrich

Description and Significance
We are developing a new programming language, Meerkat, for distributed web apps. Meerkat is an end-to-end reactive programming language, meaning that it provides seamless reactivity not just on the front end but responds to changes in back end data as well. A type system allows Meerkat programs to be updated safely while they are running. Starting with a client-server concept developed by our collaborators [1], we are exploring the theory and implementation of making the approach scalable by keeping reactive data on a distributed data store. The end goal is to provide programmers with a safer, more scalable, and more usable programming model compared to the state of the art

Student Involvement
We anticipate that students will contribute to the design and implementation of Meerkat. Students should have taken a class (or gathered experience outside the classroom) in compilers. The project will involve some distributed systems work but can learn what they need to know as part of the internship. Depending on the interests and background of the student, there may be opportunities to extend the theoretical foundations of the system as well.

References
[1] Miguel Domingues and João Costa Seco. Type Safe Evolution of Live Systems. REBLS'15. https://docentes.fct.unl.pt/jrcs/files/rebls15.pdf

Mentors: Hanan Hibshi and Maverick Woo

Description and Significance
picoCTF is a free online Capture The Flag-style game implemented by and maintained at Carnegie Mellon University to promote and facilitate cybersecurity education. The target audience of our service has been middle and high school students since 2013, but it has also been increasingly popular and attracted many other age groups, including college students and adult learners. Each picoCTF release features ~100 cybersecurity challenge problems of increasing difficulty, which are revealed over a storyline to guide players to hone their skills one step at a time. These security challenges cover concepts such as cryptography, binary exploitation, web exploitation, reverse engineering, forensics, and other topics related to security and privacy. As a year-round education platform, the picoCTF team conducts constant research in areas including cybersecurity education methodologies, CTF problem development, and education platform development. This summer, we have multiple research projects for motivated students to get involved in various missions in picoCTF:

(1) Collect empirical data through surveys, user studies, and classroom observations
To improve the design of the picoCTF platform to reach a larger number of students, especially in under-resourced communities, we need to collect and analyze empirical data to inform our design enhancement and platform scalability process. This project includes a research plan to obtain the needed data through conducting user studies, focus groups, and usability and scalability tests that examine picoCTF in a classroom setting. We are interested in understanding how we can enhance our platform to better serve K-12 teachers and students, college students, and independent adult learners in under-resourced communities. The empirical data collected by closely observing participants in focus groups and from surveys and questionnaires will provide informed feedback to the picoCTF research team about possible technical challenges and key design improvements that would enhance the students experience.

(2) Analyze player data from previous years and develop visualization tools
In addition to the surveys and questionnaires, the current picoCTF platform is rich with player data from previous years that could be a valuable resource to conduct in-depth analysis that would help understand how to improve the game to reach a wider audience, and what/where to include new challenges. The analysis would help reveal patterns that could be mapped to educational goals and help investigate where players fail to solve challenges or where the game becomes less interesting. These findings could ultimately help improve the user experience and retainment. Other areas of analysis include performance by gender, team diversity, age, educational background, etc. We envision students will learn to use modern data analysis toolkits to analyze our data and build an interactive web-based exploration tool for presenting the findings from these analyses.

(3) Write new CTF challenges for the game and test current CTF challenges
Writing and testing CTF challenges are ongoing tasks in picoCTF. Testing current challenges help identify errors and bugs before a future competition goes live, and writing new challenges help increase our challenges pool. For the latter, we are especially interested in new challenges in areas that we have minimal or no existing coverage on our platform. These include privacy, mobile security (Android / iOS), IoT security (e.g., embedded Linux-based device), and ICS security (e.g., RTOS, ROS). Students will engage in learning security and privacy problems that arise in these areas and develop new CTF challenges of gradually increasing complexity to cater to players with different stages of technical capability.

Student Involvement
We are looking for multiple students who are interested in cybersecurity and who enjoy working on projects that have a global impact on youth and workforce development. Dr. Hanan Hibshi and Dr. Maverick Woo will be the faculty members overseeing students' research activities, and the picoCTF team consists of software engineers and graduate students who work together with student research assistants. The picoCTF project is interdisciplinary in nature and can be attractive to students with different backgrounds. Students with Human-Computer Interaction background can enjoy conducting user studies, collecting empirical data, or examining the picoCTF interface and proposing design changes that can improve user experience. Students with an interest in CS education and/or cognitive psychology could help analyze the data from existing players to investigate ways that can improve learning outcomes. Students who enjoy software development can help the technical team improve the current gaming platform and migrate to the new 2021 picoCTF that has advanced features. Finally, students with a cybersecurity background can join our team and enjoy testing the current challenges (by playing the game!) and help create new challenges or add a new category of challenges.

References
Owens, K., Fulton, A., Jones, L. and Carlisle, M., 2019. pico-Boo!: How to avoid scaring students away in a CTF competition.

Mentor: Joshua Sunshine

Description and Significance
Automatic differentiation (autodiff or AD) is a widely used technique for efficiently computing derivatives of any program that computes a numerical value. The computed derivatives can be used to determine how small perturbations in a program's inputs can effect its outputs. Gradient-based optimization uses these derivatives to determine which direction to move to optimize an objective function. These techniques are key to current work in domains such as computer graphics and machine learning.

Significant advancements in AD algorithms have resulted in systems like PyTorch, TensorFlow, and JAX. These frameworks provide high-level APIs for computing gradients of functions, making it easier for users to leverage AD in their work. The computation model of each of these popular machine learning frameworks is centered around the tensor: you must structure your program as a composition of operations on tensors. However, many programs are instead much more easily expressed using mathematical operations on scalars; we call these "pointful" programs. In addition, none of the aforementioned tools can run in a web browser. Web applications require no installation or central maintenance and can reduce security risks. When teaching students with a simulator, for instance, it is advantageous to deploy instantly to every student's web browser and to avoid exposing servers to potentially insecure code the students write. The most popular autodiff framework for the web is TensorFlow.js, which is extremely inefficient for pointful programs.

This project addresses the gap by building extensible efficient pointful autodiff technology for the web, enabling a new wave of interactive web applications for computer-aided design, Bayesian inference, physics, generative art, and more. Our current prototype is an engine called Rose, which is written in a combination of Rust and TypeScript, and allows users to define, differentiate, compile, and run functions entirely inside of a web browser.

Student Involvement
Many research directions are possible for this project! If you're interested in programming language theory, there's work to be done on the formal foundations of the language to ensure that certain properties of programs are preserved when taking derivatives. If you're interested in system-building, there's work to be done on the implementation itself to make it faster, more general, and nicer to use. If you're interested in human-computer interaction, there's work to be done in studying how easy it is for people to write and debug differentiable programs. Come build the future of interactive differentation with us!

References
Rose: https://github.com/rose-lang/rose

Mentors: Norman Sadeh, Hana Habib and Lorrie Cranor

Description and Significance
The goal of the Privacy & AI Threat Modeling Project is to develop and evaluate methodologies and design patterns to help companies systematically identify and mitigate potential privacy and AI threats as they design and develop new products and services. The project focuses on threats associated with the need to provide users with adequate notices and controls over the technologies with which they interact.

Addressing privacy threats and threats associated with the development of AI solutions is becoming an increasingly significant challenge for industry. Companies are in desperate need for frameworks and methodologies that can help them systematically identify threats and approaches to mitigate such threats (e.g., providing notices and controls that are easily accessible, that are informative and understandable, that are non-manipulative, etc.)

Student Involvement
Students will learn to model new products and services and will help evaluate & refine methodologies developed as part of this project. This work will likely involve conducting human subject studies designed to evaluate the usability of design patterns for notices and controls. This project will involve working under the supervision of several faculty and a post-doctoral researcher and may involve collaborating with other students too.

Related Publications
Y Feng, Y Yao, N Sadeh , A design space for privacy choices: Towards meaningful privacy control in the internet of things, Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems

H Habib, LF Cranor, Evaluating the usability of privacy choice mechanisms
Eighteenth Symposium on Usable Privacy and Security (SOUPS 2022), 273-289

Mentor: Norman Sadeh

Description and Significance
Security and privacy are becoming increasingly complex to manage for everyday users. The need for effective assistants capable of effectively helping users in this area has never been more important.

Increasingly users are turning to chatbots to answer a variety of everyday security and privacy questions. The objective of this project is to develop personalized GenAI assistants capable of providing users with personalized answers that are not just accurate but that also reflect their level of expertise, are understandable and actionable, and motivate them to heed the assistant's recommendations.

Student Involvement
Students working in this project will learn to systematically evaluate and refine GenAI technologies in the context of security and privacy questions. This will include work designed to increase the accuracy of provided answers as well as work designed to elicit more effective answers.

Recent Publications
Breaking down walls of text: How can nlp benefit consumer privacy?
A Ravichander, A Black, T Norton, S Wilson, N Sadeh
ACL, 2021

Question answering for privacy policies: Combining computational and legal perspectives
A Ravichander, AW Black, S Wilson, T Norton, N Sadeh, EMNLP 2019.
arXiv preprint arXiv:1911.00841

Mentor: Norman Sadeh

Description and Significance
With the increasingly widespread deployment of sensors recording and interpreting data about our every moves and activities, it has never been more important to develop technology that enables people to retain some level of awareness and control over the collection and use of their data. While doing so as users browse the Web or interact with their smartphones is already proving to be daunting, it is even more challenging when data collection takes place through sensors such as cameras, microphones and other technologies users are unlikely to even notice. CMU's Privacy Infrastructure for the Internet of Things is designed to remedy this situation. It consists of a portal that enables owners of sensors to declare the presence of their devices, describe the data they collect and, if they want to, provide people with access to controls that enable them to possibly restrict how much data is collected about them and for what purpose. The infrastructure comes along with an IoT Assistant mobile app. The app enables people to discover sensors around them and access information about these sensors, including any available settings that might enable them to restrict the collection and use of their data. Deployed in Spring 2020, the infrastructure already hosts descriptions of well over 100,000 sensors in 27 different countries and the IoT Assistant app has been downloaded by tens of thousands of users. The objective of this project is to extend and refine some of the infrastructure's functionality.

Mentor: Steven Wu

Description and Significance
Many modern applications of machine learning (ML) rely on datasets that may contain sensitive personal information, including medical records, browsing history, and geographic locations. To protect the private information of individual citizens, many ML systems now train their models subject to the constraint of differential privacy (DP), which informally requires that no individual training example has a significant influence on the trained model. After well over a decade of intense theoretical study, DP has recently been deployed by many organizations, including Microsoft, Google, Apple, LinkedIn, and more recently the 2020 US Census. However, the majority of the existing practical deployments still focus on rather simple data analysis tasks (e.g., releasing simple counts and histogram statistics). To put DP to practice for more complex machine learning tasks, this project will study new differentially private training methods for deep learning that improve on existing state-of-the-art methods. We will also study how to use DP deep learning techniques to train deep generative models, which can generate privacy-preserving synthetic data—a collection of “fake” data that preserve important statistical properties of the original private data set. This, in turn, will enable privacy-preserving data sharing.

Mentor: Eunsuk Kang

Description and Significance
Unintuitive, badly designed human-machine interfaces (HMI) are not merely an annoyance, but can pose significant risks to users in systems where safety is a key concern. For example, poor HMI design has been attributed as a major factor in numerous fatal accidents involving medical devices, automobiles, and aviation systems. The challenge is that humans are far from perfect and inadvertently make mistakes from time to time, but many interfaces are not designed to deal with such human errors; as a result, when a safety failure occurs, it is often the users who get blamed, even when a better designed interface could have prevented such a failure. To tackle this challenge, Dr. Kang is collaborating with researchers in human factors and cognitive science to systematically design HMIs that are robust against human errors; i.e., an interface that is explicitly designed to recognize and handle potential human errors and prevent them from causing safety failures.

Student Involvement
In this project, students will contribute to the development of a new methodology for designing safe and robust HMIs. Potential research tasks include: (1) developing a theoretical foundation for robust HMIs, (2) a mathematical approach for modeling human behavior and errors, (3) an automated technique for analyzing an HMI for its robustness against human errors, and (4) an automated technique for repairing an HMI to improve its robustness. Students will also get a chance to apply these techniques to realistic case studies, including interfaces for medical devices and intelligent vehicles. Students are expected to have a basic background in logic and discrete math. Knowledge in formal methods, programming languages and/or HCI is a plus.

Mentor: Yorie Nakahira

Description and Significance
Autonomous driving system design needs to account for a lot of challenges, where one of them is dealing with occlusions in the environment. Examples of the occlusions include buildings, other vehicles, obstacles on the road, etc. Such occlusions may lead to latent risks that arise from the unobserved regions behind the occlusion. On the other hand, not all occlusions pose latent risks, and accounting for all of them may lead to overly conservative driving behaviors (e.g., not moving at all). To this end, we aim to identify the occlusions that should be considered when making control decisions. The overall pipeline consists of 3 steps: data generation (labeling), model training, and integration with existing results on developing control systems in the presence of occlusions.

Student Involvement
In the first step, the students will conduct experiments with an end-to-end autonomous vehicle simulator, CARLA. This practical experience involves configuring appropriate driving scenarios that facilitate collecting data about driving safety in the presence of occlusions. The students will actively work on generated occlusion data and associated labels. These data will include two types of sensor input, LiDAR and camera. The second step involves the training using existing deep neural network models, focusing on the perception-to-control aspect, that identifies the control critical occlusions from the LiDAR and/or camera data. In the third step, the students will help integrate the developed identification models into the existing results about control in the presence of occlusion and pedestrian interactions to develop an integrated autonomous driving system in occluded environments.

Mentor: Brad Myers

Description and Significance
We have developed a new way to test how well a scrolling technique works, and we need to re-implement some older techniques to see how they compare. For example, the original Macintosh scrollbars from 1984 had arrows at the top and bottom, and a draggable indicator in the middle. Even earlier scrollbars worked entirely differently. I am hoping to recruit one good programmer to help recreate some old scrolling techniques, and possibly try out some brand new ones, like for Virtual Reality applications, to test how well they do compared to regular scrolling techniques like two-fingers on a touchpad or smartphone screen. If there is time, the project will include running user tests on the implemented techniques, and writing a CHI paper based in part on the results.

Student Involvement
The student on this project will be implementing all of the techniques as web applications. The student on this project must be an excellent programmer in JavaScript or TypeScript, preferably with expertise in React or other web framework. Experience with running user studies would be a plus.

References
Paper draft: Chaoran Chen, Brad A Myers, Cem Ergin, Emily Porat, Sijia Li, Chun Wang, "ScrollTest: Evaluating Scrolling Speed and Accuracy." arXiv:2210.00735 https://arxiv.org/abs/2210.00735.

Existing test: https://charliecrchen.github.io/scrolling-test/

Mentor: Limin Jia

Description and Significance
Many web applications collect users' sensitive data, store it, and process it in the backend. To protect users' data, it is thus important to (1) detect vulnerabilities in web applications that could leak users' data or enable injection attacks and (2) build mechanisms to stop the attacks. In this project, we will investigate applying information flow security principles to solve this problem. For different parts of the web applications (client side vs. server side), we will adapt information flow security methodologies to either detect vulnerabilities or enforce security properties.

Student Involvement
The student on this project can learn information flow security principles and how to apply them to analyze real-world applications. The student can choose to be more involved in developing theories of information flow security monitors or in building analysis tools and run experiments on real-world dataset.

References
Tainted Secure Multi-Execution to Restrict Attacker Influence. ACM CCS 2023 https://dl.acm.org/doi/10.1145/3576915.3623110

NodeMedic: End-to-End Analysis of Node.js Vulnerabilities with Provenance Graphs. IEEE EURO S&P 2023 https://www.computer.org/csdl/proceedings-article/eurosp/2023/651200b101/1OFti0uB2dq

Mentor: Christian Kästner

Description and Significance
Essentially all software uses open source libraries and benefits incredibly from this publicly available infrastructure. However, with reusing libraries also come risks. Libraries may contain bugs and vulnerabilities and sometimes are abandoned; worse malicious actors are increasingly starting to attack software systems by hijacking libraries and injecting malicious code (e.g., see event-stream, Solarwinds, and ua-parser-js). Most projects use many libraries and those libraries have dependencies on their own and we also depend on all kinds of infrastructure, such as compilers and test framework, all of which could be attacked. Detected software supply chain attacks have increased 650% in 2021, after a 430% increase in 2020. This has gotten to the point that the government has stepped in and requires software companies to build a “Software Bill of Material (SBoM)” as a first step to identify what libraries are actually used.

So how can we trust this *software supply chain*, even though we have no contractual relations with the developers of all those libraries? Research might involve studying how developers build trust, when trust is justified, what attacks can be automatically detected and mitigated (e.g., with sandboxing and reproducible builds), and what actual attacks in the real world look like. There is a large range of possible research directions from code analysis to empirical studies of developers and their relationships, each of which can help to secure open source supply chains.

Student Involvement
Depending on student interest, we will investigate different ideas around software supply chains. For example, we could study how the concept of “trust” translates from organizational science to software security in an open source context and how open source maintainers make decisions about security risks (literature analysis, theory building, interviews/survey), see [1] on trust in a different context. We could build tools that automatically sandbox Javascript dependencies and evaluate the overhead of doing so, see [2] for some related prior work. We could study packages removed from npm to identify what typical supply chain attacks look like in practice. The ideal student for this project is interested in open source and software security.

References
[1] Jacovi, Alon, Ana Marasović, Tim Miller, and Yoav Goldberg. "Formalizing trust in artificial intelligence: Prerequisites, causes and goals of human trust in AI." Proc. FAccT (2021).

[2] Gabriel Ferreira, Limin Jia, Joshua Sunshine, and Christian Kästner. Containing Malicious Package Updates in npm with a Lightweight Permission System. In Proceedings of the 43rd International Conference on Software Engineering (ICSE), pages 1334--1346, Los Alamitos, CA: IEEE Computer Society, May 2021.

Mentor: Sauvik Das

Description and Significance
How can we balance the power dynamics of AI in favor of everyday Internet users, particularly those from populations who are disproportionately harmed by automated algorithmic surveillance? The subversive AI project, led by Dr. Sauvik Das, employs human-centered design processes to explore ways we can build tools and communities that help people reclaim ownership of their personal data and experiences online. Projects that we envision students helping with include: developing usable anti-facial recognition mobile camera applications, developing tools for writers to understand if their propietary content might be in the training set of large language models, developing strategies for content creators to "poison" their data in a manner that would disrupt its use in training data pipelines, and establishing/running AI self-defense clinics around the Pittsburgh area.

Mentors: Bogdan Vasilescu and Christian Kästner

Description and Significance
Reuse of open source artifacts in software ecosystems has enabled significant advances in development efficiencies as developers can now build on significant infrastructure and develop apps or server applications in days rather than months or years. However, despite its importance, maintenance of this open source infrastructure is often left to few volunteers with little funding or recognition, threatening the sustainability of individual artifacts, such as OpenSSL, or entire software ecosystems. Reports of stress and burnout among open source developers are increasing. The teams of Dr. Kaestner and Dr. Vasilecu have explored dynamics in software ecosystems to expose differences, understand practices, and plan interventions [1,2,3,4]. Results indicate that different ecosystems have very different practices and interventions should be planned accordingly [1], but also that signaling based on underlying analyses can be a strong means to guide developer attention and affect change [2]. This research will further explore sustainability challenges in open source with particular attention to the interaction between paid and volunteer contributors and stress and resulting turnover.

Student Involvement
Students will empirical study sustainability problems and interventions, using interviews, surveys, and statistical analysis of archival data (e.g., regression modeling, time series analysis for causal inference). What are the main reasons for volunteer contributors to drop out of open source projects? In what situations do volunteer contributors experience stress? In which projects will other contributors step up and continue maintenance when the main contributors leave? Which past interventions, such as contribution guidelines and code of conducts, have been successful in retaining contributors and easing transitions? How to identify subcommunities within software ecosystems that share common practices and how do communities and subcommunities learn from each other? Students will investigate these questions by exploring archival data of open source development traces (ghtorrent.org), will design interviews or surveys, will apply statistical modeling techniques, will build and test theories, and conduct literature surveys. Students will learn state of the art research methods in empirical software engineering and apply them to specific sustainability challenges of great importance. Students will actively engage with the open source communities and will learn to communicate their results to both academic and nonacademic audiences.

References
[1] Christopher Bogart and Christian Kästner and James Herbsleb and Ferdian Thung. How to Break an API: Cost Negotiation and Community Values in Three Software Ecosystems. In Proc. Symposium on the Foundations of Software Engineering (FSE), 2016.

[2] Asher Trockman, Shurui Zhou, Christian Kästner, and Bogdan Vasilescu. Adding sparkle to social coding: an empirical study of repository badges in the npm ecosystem. In Proc. International Conference on Software Engineering (ICSE), 2018.

[3] Bogdan Vasilescu, Kelly Blincoe, Qi Xuan, Casey Casalnuovo, Daniela Damian, Premkumar Devanbu, and Vladimir Filkov. The sky is not the limit: multitasking across github projects. In Proc. International Conference on Software Engineering (ICSE), 2016.

[4] Bogdan Vasilescu, Daryl Posnett, Baishakhi Ray, Mark GJ van den Brand, Alexander Serebrenik, Premkumar Devanbu, and Vladimir Filkov. Gender and tenure diversity in GitHub teams. In Proc. ACM Conference on Human Factors in Computing Systems (CHI), 2015.

Mentor: Lorrie Cranor

Description and Significance
Teenagers (children aged 13 to 17) increasingly use computing technology for education and entertainment [1]]. While they may be technically competent, a lack of life experience and a still-developing brain may place them at an increased risk of falling victim to online safety risks [2]. In particular, teens generally have a higher level of impulsivity and sensation-seeking that may lead to increased risk-taking online [3, pgs. 528-530]. Much prior work in the child safety literature has focused on issues such as cyberbullying [4] or online sexual exploitation [5]. In this project, we will explore how teenagers handle more traditional computer security challenges (e.g., avoiding fraud, maintaining secure authentication, etc.). This research could also involve developing interventions to improve teenagers’ understanding of online security. Ultimately, we hope to contribute to making the Internet a safer place for all people.

Student Involvement
Students will work with a graduate student to conduct a user study related to teens' security behavior. Through this process, they will learn about how HCI research methods (e.g., interviews, surveys, etc.) are applied to computer security and privacy issues. Based on student interest and the results of ongoing research, students may be involved in all stages of the research process, including design, execution, and analysis.

References
Emily A. Vogels, Risa Gelles-Watnick, and Navid Massarat. “Teens, Social Media and Technology 2022,” Pew Research Center, https://www.pewresearch.org/internet/2022/08/10/teens-social-media-and-technology-2022/

Diana Freed, Natalie N. Bazarova, Sunny Consolvo, Eunice J Han, Patrick Gage Kelley, Kurt Thomas, and Dan Cosley. (2023). Understanding Digital-Safety Experiences of Youth in the U.S. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems (CHI '23). Association for Computing Machinery, New York, NY, USA, Article 191, 1–15. https://doi.org/10.1145/3544548.3581128

Laura Berkand Adena Meyers. Infants, Children, and Adolescents, 8th Ed. (2016) Pearson
Olweus, Dan, and Susan P. Limber. (2018) "Some problems with cyberbullying research." Current opinion in psychology 19

Whittle, Helen, Catherine Hamilton-Giachritsis, Anthony Beech, and Guy Collings. (2013) "A review of online grooming: Characteristics and concerns." Aggression and violent behavior 18, no. 1.

Mentor: Fei Fang

Description and Significance
Congestion due to continual growth in traffic demand is one of the key challenges faced by transportation systems today. Among the various mechanisms that can alleviate congestion, one that has received substantial attention from both industry and academia is the optimization of traffic signals. On one hand, companies and municipalities are making substantial investments in deploying next-generation signal control technologies; on the other hand, researchers have developed a series of advanced AI methods – mostly in multi-agent deep reinforcement learning – to design increasingly performant signal control algorithms. But there has been very little crossover between these two streams of progress. We believe that one primary cause for this is that researchers have considered traffic signal control as more of a motivating problem than a deployment context, resulting in many assumptions being made that are incompatible with reality. In 2022, we published a workshop paper [1] that reviewed some of these assumptions, as well as some of the scattershot progress toward addressing them that researchers have made. Now, our goal is to expand this paper into a more comprehensive review and call to action for researchers so that their algorithms can make tangible impacts on transportation systems.

Student Involvement
The student will take on a primary role in performing a systematic review of traffic signal control in practice and as a problem formulation for reinforcement learning. We expect that the student will be able to go beyond the challenges we outlined in the workshop version of the review paper to comprehensively identify discrepancies that could arise at different stages in the AI deployment pipeline. Overall, this will be a project with a focus on literature review, but it will also likely involve informal engagement with industry stakeholders to better understand their deployment needs. Having a basic background in reinforcement learning is preferred, but we intend for this project to serve as a gentle introduction to problem formulation and literature reviews for AI research.

References
[1] Rex Chen, Fei Fang, & Norman Sadeh (2022) “The Real Deal: A Review of Challenges and Opportunities in Moving Reinforcement Learning-Based Traffic Signal Control Systems Towards Reality”. 12th International Workshop on Agents in Traffic and Transportation (ATT ’22 @ IJCAI ’22), CEUR Workshop Proceedings 3173: 14–31.

Mentor: Lorrie Cranor

Description and Significance
The goal of Distributed Confidential Computing (DCC) is to enable scalable data-in-use protections for cloud and edge systems, like home IoT. An important aspect of DCC is ensuring that data use adheres to specific policies. Typically, these policies are written in technical languages, like formal logic, which makes it impractical for non-experts to write their own policies. The goal of this project is to (1) determine what kind of policies home IoT users would want to express for their own data, and (2) how they can communicate these policies so that they can be verified by the DCC technology, without being too technical to be understood by the user.

Student Involvement
Students will learn how to conduct research in usable privacy and security by working with a postdoc to conduct a user study that will identify privacy preferences of home IoT users. Based on this data, the team will design and implement prototype policy interfaces, which can be evaluated by another user study. Depending on interests and project needs, the student may help set up online surveys and collect data on a crowd worker platform, perform qualitative and/or quantitative data analysis, or design and implement prototypes.

References
Center for Distributed Confidential Computing. https://nsf-cdcc.org/

Hana Habib and Lorrie Faith Cranor. Evaluating the Usability of Privacy Choice Mechanisms. SOUPS ‘22. https://www.usenix.org/system/files/soups2022-habib.pdf

McKenna McCall, Eric Zeng, Faysal Hossain Shezan, Mitchell Yang, Lujo Bauer, Abhishek Bichhawat, Camille Cobb, Limin Jia, and Yuan Tian. Towards Usable Security Analysis Tools for Trigger-Action Programming. SOUPS ‘23. https://www.usenix.org/system/files/soups2023-mccall.pdf

Mentor: Bryan Parno

Description and Significance
Rust is already a rapidly growing mainstream language (e.g., with users in Amazon, Google, Microsoft, Mozilla, and the Linux kernel) designed to produce "more correct" low-level systems code. Rust supports writing fast systems code, with no runtime or garbage collection, but its powerful type system and ownership model guarantee memory- and thread-safety. This alone can rule out a large swath of common vulnerabilities. However, it does nothing to rule out higher-level vulnerabilities, like SQL injection, incorrect crypto usage, or logical errors.

Hence, we are developing a language and tool called Verus, which allows Rust developers to annotate their code with logical specifications for the code's behavior, and it automates the process of mathematically proving that the code meets those specifications. This means we can guarantee the code's correctness, reliability, and/or security at compile time.

Student Involvement
In this project, students will learn more about software verification, write code in Verus and prove it correct, and work to make Verus even easier for developers to use.

References
Verus: https://github.com/verus-lang/verus
Rust: https://www.rust-lang.org/
Our Research Lab: https://www.andrew.cmu.edu/user/bparno/research.html

Mentors: Joshua Sunshine and Eunsuk Kang

Description and Significance
Formal specifications play a crucial role in providing robust assurance to systems by offering a rigorous and unambiguous description of system requirements, behaviors, and properties. Under this framework, one can write a set of specifications that describe the desired properties, and use tools like Alloy [1] to automatically check these specifications in a system (model).

With the increasing prevalence of AI / LLMs and automatic code generation, writing “good” specifications that reflect what the users want of a system is more important than ever. However, these specifications are often hard to understand, develop, and debug with the current tools.

One hypothesis is that visualizations can help humans check, validate, and debug elements of specifications. With the help of a “good” diagram, one can easily spot parts of the diagram that do not make sense, potentially uncovering some bugs in the underlying specifications. Alloy, for example, has a built-in default visualizer that displays all models and instances as node-edge graphs. While they can be useful, this level of visualization abstraction (nodes and edges) may not be suitable for all domains. For example, a communication protocol between two machines or processes may best be visualized as a sequence diagram [2].

The goal of this project is to study reusable domain-specific visualizations with the help of Penrose [3][4], a programming language that converts abstract expressions into diagrams. Aside from hand-creating domain-specific visualizations for specifications in Penrose, we will also investigate how to automatically convert these specifications to visualizations. This project may also involve making contributions to the Penrose codebase to better suit our needs and evaluating the extent to which these domain-specific visualizations help users of formal specification tools.

It is recommended that students have familiarity with discrete math and logic.

References
[1] Daniel Jackson. 2016. Software abstractions: Logic, language, and analysis, MIT Press.

[2] See examples of sequence diagrams at https://mermaid.js.org/syntax/sequenceDiagram.html

[3] Dor Ma'ayan, Wode Ni, Katherine Ye, Chinmay Kulkarni, and Joshua Sunshine. 2020. How Domain Experts Create Conceptual Diagrams and Implications for Tool Design. In Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems (CHI '20). Association for Computing Machinery, New York, NY, USA, 1–14. https://doi.org/10.1145/3313831.3376253

[4] Katherine Ye, Wode Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan Crane. 2020. Penrose: from mathematical notation to beautiful diagrams. ACM Trans. Graph. 39, 4, Article 144 (August 2020), 16 pages. https://doi.org/10.1145/3386569.3392375