Automated static dataflow analysis is an effective technique for detecting security critical issues like sensitive data leak, and vulnerability to injection attacks. Ensuring high precision and recall requires an analysis that is context, field and object sensitive. However, it is challenging to attain high precision and recall and scale to large industrial code bases. Compositional style analyses in which individual software components are analyzed separately, independent from their usage contexts, compute reusable summaries of components. This is an essential feature when deploying such analyses in CI/CD at code-review time or when scanning deployed container images. In both these settings the majority of software components stay the same between subsequent scans. However, it is not obvious how to extend such analyses to check the kind of contextual taint specifications that arise in practice, while maintaining compositionality. In this work we present contextual dataflow modeling, an extension to the compositional analysis to check complex taint specifications and significantly increasing recall and precision. Furthermore, we show how such high-fidelity analysis can scale in production using three key optimizations: (i) discarding intermediate results for previously-analyzed components, an optimization exploiting the compositional nature of our analysis; (ii) a scope-reduction analysis to reduce the scope of the taint analysis w.r.t. the taint specifications being checked, and (iii) caching of analysis models. We show a 9.85% reduction in false positive rate on a comprehensive test suite comprising the OWASP open-source benchmarks as well as internal real-world code samples. We measure the performance and scalability impact of each individual optimization using open source JVM packages from the Maven central repository and internal AWS service codebases. This combination of high precision, recall, performance, and scalability has allowed us to enforce security policies at scale both internally within Amazon as well as for external customers.

Smalltalk, one of the first object-oriented programming languages, has had a tremendous influence on the evolution of computer technology. Due to the simplicity and productivity provided by the language, Smalltalk is still in active use today by many companies with large legacy codebases and with new code written every day. A crucial problem in Smalltalk programming is the race condition. Like in any other parallel language, debugging race conditions is inherently challenging, but in Smalltalk, it is even more challenging due to its dynamic nature. Being a purely dynamically-typed language, Smalltalk allows assigning any object to any variable without type restrictions, and allows forking new threads to execute arbitrary anonymous code blocks passed as objects. In Smalltalk, race conditions can be introduced easily, but are difficult to prevent at runtime. We present SmallRace, a novel static race detection framework designed for multithreaded dynamic languages, with a focus on Smalltalk. A key component of SmallRace is SmallIR, a subset of LLVM IR, in which all variables are declared with the same type-a generic pointer 18✶. This allows SmallRace to design an effective interprocedural thread-sensitive pointer analysis to infer the concrete types of dynamic variables. SmallRace automatically translates Smalltalk source code into SmallIR, supports most of the modern Smalltalk syntax in Visual Works, and generates actionable race reports with detailed debugging information. Importantly, SmallRace has been used to analyze a production codebase in a large company with over a million lines of code, and it has found tens of complex race conditions in the production code.

Solana is a rapidly-growing high-performance blockchain powered by a Proof of History (PoH) consensus mechanism and a novel stateless programming model that decouples code from data. With parallel execution on the PoH Sealevel runtime (instead of PoW), it achieves 100X-1000X speedups compared to Ethereum in terms of transactions per second. With the new programming model, new constraints (owner, signer, keys, bump seeds) and vulnerabilities (missing checks, overflows, type confusion, etc.) must be carefully verified to ensure the security of Solana smart contracts. This paper proposes VRust, the first automated smart contract vulnerability detection framework for Solana. A key technical novelty is a set of static analysis rules for validating untrustful input accounts that are unique in the Solana programming model. We have developed a total of eight different vulnerability types, and VRust is able to check all of them fully automatically by translating source code into Rust MIR-based inference rules without any code annotations. VRust has been evaluated on over a hundred of Solana projects, and it has revealed 12 previously unknown vulnerabilities, including 3 critical vulnerabilities in the official Solana Programming Library confirmed by core developers.

Memory disaggregation has risen in popularity in datacenters due to benefits such as higher utilization and better hardware elasticity. However, applications running on memory disaggregated clusters commonly suffer from data amplification---I/O traffic is grossly increased due to (4KB-)page-based swapping mechanism in the OS, causing excessive data roundtrips to remote memory. There has been work proposing finer-granularity swapping to support memory disaggregated clusters. However, these efforts face practicality challenges: they either require not-yet-available hardware or force developers to go through a labor-intensive process of rewriting existing programs. This paper introduces SemSwap, an ongoing work that aims to mitigate data amplification in a practical manner---no hardware nor heavyweight refactoring is required. We propose a cross-layer technique that transparently passes program semantics (e.g., data hotness) collected at the runtime level to the kernel to reduce remote memory access cost. Specifically, we consolidate "hot" objects that are frequently accessed onto a single memory page before these pages are swapped out to remote memory. The subsequent memory accesses will be much more effective as hot data are readily in memory. Hence, SemSwap reduces the total number of remote memory fetches, leading to faster execution. We also present an implementation plan and an evaluation plan for SemSwap in this paper.

In this paper, we work towards linking users’ identities on different social media platforms by exploring the user-generated contents (UGCs). This task is non-trivial due to the following challenges. 1) As UGCs involve multiple modalities (e.g., text and image), how to accurately characterize the user account based on their heterogeneous multi-modal UGCs poses the main challenge. 2) As people tend to post similar UGCs on different social media platforms during the same period, how to effectively model the temporal post correlation is a crucial challenge. And 3) no public benchmark dataset is available to support our user identity linkage based on heterogeneous UGCs with timestamps. Towards this end, we present an attentive time-aware user identity linkage scheme, which seamlessly integrates the temporal post correlation modeling and attentive user similarity modeling. To facilitate the evaluation, we create a comprehensive large-scale user identity linkage dataset from two popular social media platforms: Instagram and Twitter. Extensive experiments have been conducted on our dataset and the results verify the effectiveness of the proposed scheme. As a residual product, we have released the dataset, codes, and parameters to facilitate other researchers.

Python type inference is challenging in practice. Due to its dynamic properties and extensive dependencies on third-party libraries without type annotations, the performance of traditional static analysis techniques is limited. Although semantics in source code can help manifest intended usage for variables (thus help infer types), they are usually ignored by existing tools. In this paper, we propose PYInfer, an end-to-end learning-based type inference tool that automatically generates type annotations for Python variables. The key insight is that contextual code semantics is critical in inferring the type for a variable. For each use of a variable, we collect a few tokens within its contextual scope, and design a neural network to predict its type. One challenge is that it is difficult to collect a high-quality human-labeled training dataset for this purpose. To address this issue, we apply an existing static analyzer to generate the ground truth for variables in source code. Our main contribution is a novel approach to statically infer variable types effectively and efficiently. Formulating the type inference as a classification problem, we can handle user-defined types and predict type probabilities for each variable. Our model achieves 91.2% accuracy on classifying 11 basic types in Python and 81.2% accuracy on classifying 500 most common types. Our results substantially outperform the state-of-the-art type annotators. Moreover, PYInfer achieves 5.2X more code coverage and is 187X faster than a state-of-the-art learning-based tool. With similar time consumption, our model annotates 5X more variables than a state-of-the-art static analysis tool. Our model also outperforms a learning-based function-level annotator on annotating types for variables and function arguments. All our tools and datasets are publicly available to facilitate future research in this direction.