As Python is increasingly being adopted for large and complex programs, the importance of static analysis for Python (such as type inference) grows. Unfortunately, static analysis for Python remains a challenging task due to its dynamic language features and its abundant external libraries. To help fill this gap, this paper presents PoTo, an Andersen-style context-insensitive and flow-insensitive points-to analysis for Python. PoTo addresses Python-specific challenges and works for large programs via a novel hybrid evaluation, integrating traditional static points-to analysis with concrete evaluation in the Python interpreter for external library calls. Next, this paper presents PoTo+, a static type inference for Python built on the points-to analysis. We evaluate PoTo+ and compare it to two state-of-the-art Python type inference techniques: (1) the static rule-based Pytype and (2) the deep-learning based DLInfer. Our results show that PoTo+ outperforms both Pytype and DLInfer on existing Python packages.

Multimodal Large Language Models (LLMs) are pivotal in revolutionizing customer support and operations by integrating multiple modalities such as text, images, and audio. Federated Prompt Learning (FPL) is a recently proposed approach that combines pre-trained multimodal LLMs such as vision-language models with federated learning to create personalized, privacy-preserving AI systems. However, balancing the competing goals of personalization, generalization, and privacy remains a significant challenge. Over-personalization can lead to overfitting, reducing generalizability, while stringent privacy measures, such as differential privacy, can hinder both personalization and generalization. In this paper, we propose a Differentially Private Federated Prompt Learning (DP-FPL) approach to tackle this challenge by leveraging a low-rank factorization scheme to capture generalization while maintaining a residual term that preserves expressiveness for personalization. To ensure privacy, we introduce a novel method where we apply local differential privacy to the two low-rank components of the local prompt, and global differential privacy to the global prompt. Our approach mitigates the impact of privacy noise on the model performance while balancing the tradeoff between personalization and generalization. Extensive experiments demonstrate the effectiveness of our approach over other benchmarks.

Abstract Application programming interfaces often have correctness constraints that cut across multiple arguments. Violating these constraints causes the underlying code to raise runtime exceptions, but at the interface level, these are usually documented at most informally. This article presents novel principled static analysis and the first interprocedural weakest‐precondition analysis for Python to extract inter‐argument constraints. The analysis is mostly static, but to make it tractable for typical Python idioms, it selectively switches to the concrete domain for some cases. This article focuses on the important case where the interfaces are machine‐learning operators and their arguments are hyperparameters, rife with constraints. We extracted hyperparameter constraints for 429 functions and operators from 11 libraries and found real bugs. We used a methodology to obtain ground truth for 181 operators from 8 machine‐learning libraries; the analysis achieved high precision and recall for them. Our technique advances static analysis for Python and is a step towards safer and more robust machine learning.

Recent years have witnessed significant advances in programming technology for multi-party computation (MPC), bringing MPC closer to practice and wider applicability. Typical MPC programming frameworks focus on either front-end language design (e.g., Wysteria, Viaduct, SPDZ), or back-end protocol design and implementation (e.g., ABY, MOTION, MP-SPDZ).

Machine-learning operators often have correctness constraints that cut across multiple hyperparameters and/or data. Violating these constraints causes the operator to raise runtime exceptions, but those are usually documented only informally or not at all. This paper presents the first interprocedural weakest-precondition analysis for Python to extract hyperparameter constraints. The analysis is mostly static, but to make it tractable for typical Python idioms in machine-learning libraries, it selectively switches to the concrete domain for some cases. This paper demonstrates the analysis by extracting hyperparameter constraints for 181 operators from a total of 8 ML libraries, where it achieved high precision and recall and found real bugs. Our technique advances static analysis for Python and is a step towards safer and more robust machine learning.

While Python is increasingly popular, program analysis tooling for Python is lagging. This is due, in part, to complex features of the Python language---features with difficult to understand and model semantics. Besides the "usual suspects", reflection and dynamic execution, complex Python features include context managers, decorators, and generators, among others. This paper explores how often and in what ways developers use certain complex features. We analyze over 3 million Python files mined from GitHub to address three research questions: (i) How often do developers use certain complex Python features? (ii) In what ways do developers use these features? (iii) Does use of complex features increase or decrease over time? Our findings show that usage of dynamic features that pose a threat to static analysis is infrequent. On the other hand, usage of context managers and decorators is surprisingly widespread. Our actionable result is a list of Python features that any "minimal syntax" ought to handle in order to capture developers' use of the Python language. We hope that understanding the usage of Python features will help tool-builders improve Python tools, which can in turn lead to more correct, secure, and performant Python code.

Python 3 is a highly dynamic language, but it has introduced a syntax for expressing types with PEP484. This paper explores how developers use these type annotations, the type system semantics provided by type checking and inference tools, and the performance of these tools. We evaluate the types and tools on a corpus of public GitHub repositories. We review MyPy and PyType, two canonical static type checking and inference tools, and their distinct approaches to type analysis. We then address three research questions: (i) How often and in what ways do developers use Python 3 types? (ii) Which type errors do developers make? (iii) How do type errors from different tools compare?

Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a type-based reachability analysis that accounts for mutable heap data. The underlying semantics of FlowCFL is Context-Free-Language (CFL)-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability analysis. Second, we establish correctness of CFL-reachability over graphs with inverse edges (inverse edges are necessary for the handling of mutable heap data). Our approach combines CFL-reachability with reference immutability to avoid the addition of certain inverse edges, which results in graph reduction and precision improvement. The key contribution of our work is the formal account of correctness, which extends to the case when inverse edges are removed. Third, we present a type-based reachability analysis and establish equivalence between a certain CFL-reachability analysis and the type-based analysis, thus proving correctness of the type-based analysis.

Multi-party computation (MPC) protocols have been extensively optimized in an effort to bring this technology to practice, which has already started bearing fruits.The choice of which MPC protocol to use depends on the computation we are trying to perform.Protocol mixing is an effective black-box -with respect to the MPC protocols-approach to optimize performance.Despite, however, considerable progress in the recent years existing works are heuristic and either give no guarantee or require an exponential (bruteforce) search to find the optimal assignment, a problem which was conjectured to be NP hard.We provide a theoretically founded approach to optimal (MPC) protocol assignment, i.e., optimal mixing, and prove that under mild and natural assumptions, the problem is tractable both in theory and in practice for computing best two-out-of-three combinations.Concretely, for the case of two protocols, we utilize program analysis techniques-which we tailor to MPC-to define a new integer program, which we term the Optimal Protocol Assignment (in short, OPA) problem whose solution is the optimal (mixed) protocol assignment for these two protocols.Most importantly, we prove that the solution to the linear program corresponding to the relaxation of OPA is integral, and hence is also a solution to OPA.Since linear programming can be efficiently solved, this yields the first efficient protocol mixer.We showcase the quality of our OPA solver by applying it to standard benchmarks from the mixing literature.Our OPA solver can be applied on any two-out-of-three protocol combinations to obtain a best two-out-of-three protocol assignment.

Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable reference may be mutable due to approximation. In this paper, we present ReM (for definite Re[ference] M[utability]). It separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all mutable references are definitely mutable.

In cloud computing customers upload data and computation to cloud providers. As they cede their data to the cloud provider, they may cede data confidentiality. We develop SecureMR, a system that analyzes and transforms MapReduce programs to operate over encrypted data. SecureMR makes use of partially homomorphic encryption and a trusted client. We evaluate SecureMR on a set of MapReduce benchmarks.

Submitty is an open source programming assignment submission system from the Rensselaer Center for Open Source Software (RCOS) at Rensselaer Polytechnic Institute (RPI) accessed via an online interface. Submitty allows students to submit their code through file upload or version control, such as an internal Git/SVN server or Github, where it is then tested with a highly configurable and customizable automated grader. For each assignment, instructors can specify whether or not students can work in teams. For team assignments, the instructor can either assign teammates or allow the students to choose. In addition to the auto-grading for submissions, Submitty supports human grading. The human graded rubric is developed by the graders as they work, allowing reuse of common feedback messages and partial credit points. The rubric can be searched and modified during and after grading is complete for consistency. By default, grading is handled by instructors and TAs who are assigned to sections of students, which can be rotated through the semester. However, an instructor can choose to incorporate peer grading, which will allow students to anonymously view and submit grades for each other, receiving multiple peer grades per assignment. Submitty has been used at RPI for several years for a variety of courses, serving over 1500 students and 50 instructors and TAs each semester, and has recently been used by several other universities. We will present "case studies" of assignment configurations for autograding and manual grading and demonstrate the grading interface in support of team submissions and peer grading.

With surging enrollment in Computer Science courses at both the introductory and advanced level, it is critical to leverage automated testing and grading to ensure consistent assessment of student learning. Program analysis tools allow us to streamline the grading process so instructors and TAs can spend more time teaching, one-on-one tutoring, and mentoring students. We present complex use cases of automated assignment testing and grading within the open-source homework submission system, Submitty. Students receive immediate and detailed feedback from the automated grader, and can resubmit to correct errors. Submitty uses custom-built grading tools, including difference checking of plaintext program output, instructor authored assignment-specific custom graders, and static analysis tools that reason about program structure. In addition, it employs a variety of external tools, including version control (Git and SVN), unit testing frameworks (JUnit), memory debugging tools (Valgrind and DrMemory), and code coverage tools (Emma). In this poster we describe our experience with memory debugging and code coverage tools, and outline plans to include immutability inference and verification.

Student experience in introductory computer science classes can be enhanced by applying static analysis techniques to automatically grade assignments. At Rensselaer Polytechnic Institute (RPI), introductory computer science classes (using Python) exceed 650 students in size. As resources are limited, it is infeasible to have teaching staff individually examine each student's answer for small in-lecture exercises; however, qualitative data regarding student code independent from execution is still valuable (and in some cases required) to assess progress. When static analysis utilities were made available to instructors and integrated with automatic assignment testing, instructors were able to judge student performance and provide feedback at a scale that would otherwise be infeasible.

Submitty (http://submitty.org) is an open source programming assignment submission system from the Rensselaer Center for Open Source Software (RCOS) at Rensselaer Polytechnic Institute (RPI). Students can submit their code via a web interface in a variety of ways, where it is then tested with a highly configurable and customizable automated grader. Students receive immediate feedback from the grader, and can resubmit to correct errors as needed. Through an online interface, TAs can access detailed grading results and supplement the automated scores with manual grading (numeric and written feedback) of overall program structure, good use of comments, reasonable error checking, etc. and any non-programming components of the assignment. The instructor can also configure the system to allow for a configurable late day policy on a per assignment and per student basis. We currently use Submitty in eight different courses (spanning from introductory through advanced topics) serving over 1500 students and 35+ instructors and TAs each week. We will present a range of "case study" assignment configurations in a hands-on demo, going from simple through complex, using a variety of different automated grading methods including per-character and per-line output difference checkers, external unit testing frameworks (such as JUnit), memory debugging tools (Valgrind and DrMemory), code coverage (e.g., Emma), static analysis tools, and custom graders. Submitty can be customized per test case as appropriate to apply resource limits (running time, number of processes, output file size, etc.) and to display or hide from students the program output, autograding results, and testing logs.

We propose a type-based taint analysis for Android. Concretely, we present DFlow, a context-sensitive information flow type system, and DroidInfer, the corresponding type inference analysis for detecting privacy leaks in Android apps. We present novel techniques for error reporting based on CFL-reachability, as well as novel techniques for handling of Android-specific features, including libraries, multiple entry points and callbacks, and inter-component communication. Empirical results show that our approach is scalable and precise. DroidInfer scales well in terms of time and memory and has false-positive rate of 15.7%. It detects privacy leaks in apps from the Google Play Store and in known malware.

Information flow type systems, such as EnerJ (a type system for energy efficiency), and integrity and confidentiality, are unsound if subtyping for references is allowed because of the presence of mutable references. The standard approach is to disallow subtyping for references, or in other words, replace subtyping constraints with equality constraints. Unfortunately, this often leads to imprecision, causing the type system to reject valid programs.

Reference immutability ensures that a reference is not used to modify the referenced object, and enables the safe sharing of object structures. A pure method does not cause side-effects on the objects that existed in the pre-state of the method execution. Checking and inference of reference immutability and method purity enables a variety of program analyses and optimizations. We present ReIm, a type system for reference immutability, and ReImInfer, a corresponding type inference analysis. The type system is concise and context-sensitive. The type inference analysis is precise and scalable, and requires no manual annotations. In addition, we present a novel application of the reference immutability type system: method purity inference.

Method purity inference, also known as side-effect analysis, is an important problem. It has many applications including compiler optimization, model checking, memoization of function calls, atomicity, etc. Surprisingly, despite the long history of this problem, we know of no purity inference tool that scales to large codes and analyzes both whole programs and libraries.

Pluggable types can help find bugs such as null-pointer dereference or unwanted mutation (or they can prove the absence of such bugs). Unfortunately, pluggable types require annotations, which imposes a burden on programmers.

We present a static analysis framework for inference of security-related program properties. Within this framework we design and implement ownership, immutability and information flow inference analyses for Java. We perform empirical investigation on a set of Java components, and on a set of established security benchmarks. The results indicate that the analyses are practical and precise, and therefore can be integrated in program comprehension tools that support reasoning about software security and software quality.

This paper proposes a new static analysis for inference of explicit information flow. The analysis is context-sensitive, cubic, and works both on complete programs and software components. We perform experiments on several Java components which show that the analysis is precise and practical. Thus, the analysis can be incorporated in program understanding and verification tools and help verify security properties in a light-weight, practical manner.

We propose a mechanism for object access control which is based on the UML. Specifically, we propose use of ownership and immutability constraints on UML associations and verification of these constraints through reverse engineering. These constraints inherently support software design principles, and impose requirements on the implementation that may help prevent serious program flaws. We propose implementation-level models for ownership and immutability that capture well the meaning of these concepts in design, and we develop novel static ownership and immutability inference analyses. We perform an empirical investigation on several small-to-large Java programs. The results indicate that the inference analyses are precise and practical. Therefore, the analyses can be integrated in reverse engineering tools and can help support effective reasoning about software quality and security.

We design a new context-sensitive points-to analysis for Java thattargets key object-oriented features such as inheritance and encapsulation, and improves precision over the Andersen-style context-insensitive analysis. At the same time, it has cubic worst-case complexity, thus giving precision improvement for free.

The central paradigm of today's successful Internet is to keep the network core simple and move complexity towards the network end points. Unfortunately, this very paradigm limits network management and control capabilities, and creates opportunities for attacks such as worms, viruses, and spam that often seriously disrupt and degrade Internet and user performance. The thrust of this paper is that such problems cannot be effectively solved unless a paradigm shift is adopted. Towards a more secure and manageable Internet, we propose "virtualization" of the Internet, by carefully balancing its scalability and programmability properties. Our objective is to provide a programmable virtual Internet to users and to let them manage, control, and optimize it based on their individual needs.

Program flow analysis has many applications in software tools for program understanding, restructuring, verification, testing and reverse engineering. There are two important requirements for a flow analysis to be applied successfully in software tools: precision and practicality. We propose annotated inclusion constraints - a new general framework for formulating and implementing precise inclusion-based flow analyses. The framework can be instantiated in two dimensions: one can select a flow analysis that can be modeled using inclusion constraints (e.g., class analysis, points-to analysis) and add a dimension of precision by choosing appropriate annotations (e.g., field sensitivity, context sensitivity). The framework encompasses a large spectrum of relatively precise flow analyses. We formulate and implement several points-to analyses for Java as instances of the framework. The experiments show that precision dimensions such as field sensitivity and context sensitivity have significant impact on the points-to analysis and its clients. In the same time, using annotations to model these precision dimensions results in efficient and practical analysis. Therefore, flow analyses based on annotated constraints can be successfully incorporated in software tools.

Knowing which associations are compositions is important in a tool for the reverse engineering of UML class diagrams. Firstly, recovery of composition relationships bridges the gap between design and code. Secondly, since composition relationships explicitly state a requirement that certain representations cannot be exposed, it is important to determine if this requirement is met by component code. Verifying that compositions are implemented properly may prevent serious program flaws due to representation exposure.We propose an implementation-level composition model based on ownership and a novel approach for identifying compositions in Java software. Our approach uses static ownership inference based on points-to analysis and is designed to work on incomplete programs. In our experiments, on average 40% of the examined fields account for relationships that are identified as compositions. We also present a precision evaluation which shows that for our code base our analysis achieves almost perfect precision---that is, it almost never misses composition relationships. The results indicate that precise identification of interclass relationships can be done with a simple and inexpensive analysis, and thus can be easily incorporated in reverse engineering tools that support iterative model-driven development.

The goal of points-to analysis for Java is to determine the set of objects pointed to by a reference variable or a reference object field. We present object sensitivity , a new form of context sensitivity for flow-insensitive points-to analysis for Java. The key idea of our approach is to analyze a method separately for each of the object names that represent run-time objects on which this method may be invoked. To ensure flexibility and practicality, we propose a parameterization framework that allows analysis designers to control the tradeoffs between cost and precision in the object-sensitive analysis. Side-effect analysis determines the memory locations that may be modified by the execution of a program statement. Def-use analysis identifies pairs of statements that set the value of a memory location and subsequently use that value. The information computed by such analyses has a wide variety of uses in compilers and software tools. This work proposes new versions of these analyses that are based on object-sensitive points-to analysis.We have implemented two instantiations of our parameterized object-sensitive points-to analysis. On a set of 23 Java programs, our experiments show that these analyses have comparable cost to a context-insensitive points-to analysis for Java which is based on Andersen's analysis for C. Our results also show that object sensitivity significantly improves the precision of side-effect analysis and call graph construction, compared to (1) context-insensitive analysis, and (2) context-sensitive points-to analysis that models context using the invoking call site. These experiments demonstrate that object-sensitive analyses can achieve substantial precision improvement, while at the same time remaining efficient and practical.

This paper presents a new compile-time analysis that enables a testing methodology for white-box coverage testing of error recovery code (i.e., exception handlers) of server applications written in Java, using compiler-directed fault injection. The analysis allows compiler-generated instrumentation to guide the fault injection and to record the recovery code exercised. (An injected fault is experienced as a Java exception.) The analysis 1) identifies the exception-flow "def-uses" to be tested in this manner, 2) determines the kind of fault to be requested at a program point, and 3) finds appropriate locations for code instrumentation. The analysis incorporates refinements that establish sufficient context sensitivity to ensure relatively precise def-use links and to eliminate some spurious def-uses due to demonstrably infeasible control flow. A runtime test harness calculates test coverage of these links using an exception def-catch metric. Experiments with the methodology demonstrate the utility of the increased precision in obtaining good test coverage on a set of moderately sized server benchmarks.

This paper presents a new compile-time analysis that enables a testing methodology for white-box coverage testing of error recovery code (i.e., exception handlers) in Java web services using compiler-directed fault injection. The analysis allows compiler-generated instrumentation to guide the fault injection and to record the recovery code exercised. (An injected fault is experienced as a Java exception.) The analysis (i) identifies the exception-flow 'def-uses' to be tested in this manner, (ii) determines the kind of fault to be requested at a program point, and (iii) finds appropriate locations for code instrumentation. The analysis incorporates refinements that establish sufficient context sensitivity to ensure relatively precise def-use links and to eliminate some spurious def-uses due to demonstrably infeasible control flow. A runtime test harness calculates test coverage of these links using an exception def-catch metric. Experiments with the methodology demonstrate the utility of the increased precision in obtaining good test coverage on a set of moderately-sized Java web services benchmarks.

Testing of polymorphism in object-oriented software may require coverage of all possible bindings of receiver classes and target methods at call sites. Tools that measure this coverage need to use class analysis to compute the coverage requirements. However, traditional whole-program class analysis cannot be used when testing incomplete programs. To solve this problem, we present a general approach for adapting whole-program class analyses to operate on program fragments. Furthermore, since analysis precision is critical for coverage tools, we provide precision measurements for several analyses by determining which of the computed coverage requirements are actually feasible for a set of subject components. Our work enables the use of whole-program class analyses for testing of polymorphism in partial programs, and identifies analyses that potentially are good candidates for use in coverage tools.

Adequate testing of polymorphism in object-oriented software requires coverage of all possible bindings of receiver classes and target methods at call sites. Tools that measure this coverage need to use class analysis to compute the coverage requirements. However, traditional whole-program class analysis cannot be used when testing partial programs. To solve this problem, we present a general approach for adapting whole-program class analyses to operate on program fragments. Furthermore, since analysis precision is critical for coverage tools, we provide precision measurements for several analyses by determining which of the computed coverage requirements are actually feasible. Our work enables the use of whole-program class analyses for testing of polymorphism in partial programs, and identifies analyses that compute precise coverage requirements and therefore are good candidates for use in coverage tools.

The object relation diagram (ORD) of a program is a class interdependence diagram which has applications in a wide variety of software engineering problems (e.g., integration testing, integration coverage analysis, regression testing, impact analysis, program understanding, and reverse engineering). Because the imprecision of the ORD directly affects the practicality of its usage, it is important to investigate techniques for constructing precise ORDs. This paper makes three contributions. First, we develop the extended object relation diagram (ExtORD), a version of the ORD designed for use in integration coverage analysis. The ExtORD shows the specific statement that creates an interclass dependence, and can be easily constructed by extending techniques for ORD construction. Second, we develop a general algorithm for ORD construction, parameterized by class analysis. Third, we demonstrate empirically that relatively precise class analyses can significantly improve diagram precision compared to earlier work, resulting in average size reduction of 55% for the ORD and 39% for the ExtORD.

The goal of points-to analysis for Java is to determine the set of objects pointed to by a reference variable or a reference objet field. Improving the precision of practical points-to analysis is important because points-to information has a wide variety of client applications in optimizing compilers and software engineering tools. In this paper we present object sensitivity, a new form of context sensitivity for flow-insensitive points-to analysis for Java. The key idea of our approach is to analyze a method separately for each of the objects on which this method is invoked. To ensure flexibility and practicality, we propose a parameterization framework that allows analysis designers to control the tradeoffs between cost and precision in the object-sensitive analysis.Side-effect analysis determines the memory locations that may be modified by the execution of a program statement. This information is needed for various compiler optimizations and software engineering tools. We present a new form of side-effect analysis for Java which is based on object-sensitive points-to analysis.We have implemented one instantiation of our parameterized object-sensitive points-to analysis. We compare this instantiation with a context-insensitive points-to analysis for Java which is based on Andersen's analysis for C [4]. On a set of 23 Java programs, our experiments show that the two analyses have comparable cost. In some cases the object-sensitive analysis is actually faster than the context-insensitive analysis. Our results also show that object sensitivity significantly improves the precision of side-effect analysis, call graph construction, and virtual call resolution. These experiments demonstrate that object-sensitive analyses can achieve significantly better precision than context-insensitive ones, while at the same time remaining efficient and practical.

The goal of point-to analysis for Java is to determine the set of objects pointed by a reference variable or a reference object field. This information has a wide variety of client applications in optimizing compilers and software engineering tools. In this paper we present a point-to analysis for Java based on Andersen's point-to analysis for C [5]. We implement the analysis by using a constraint-based approach which employs annotated inclusion constraints. Constraint annotations allow us model precisely and efficiently the semantics of virtual calls and the flow of values through object fields. By solving systems of annotated inclusion constraints, we have been albe to perform practical and precies points-to analysis for Java