Search for: All records

We present BlindMarket, an end-to-end zero-trust distribution framework for hardware IP cores that operates without relying on any trusted third party. BlindMarket allows two parties, the IP user and the IP vendor, to complete an IP trading process with strong guarantees of verifiability and confidentiality before the transaction, and then traceability after. We propose verification heuristics and adapt the cone of influencebased design pruning to overcome the limited scalability common to cryptographic protocols and the hardness of the underlying hardware verification. We systematically evaluate our framework on a diverse set of real-world hardware benchmarks. The results demonstrate that BlindMarket successfully verifies 12 out of 13 IP designs and achieves substantial performance improvements enabled by design pruning and control-flow guided heuristics. 

Infrastructure as Code (IaC) has enabled cloud customers to have more agility in creating and modifying complex deployments of cloud-provisioned resources. By writing a configuration in IaC languages such as CloudFormation, users can declaratively specify their infrastructure and CloudFormation will handle the creation of the resources. However, understanding the complexity of IaC deployments has emerged as an unsolved issue. In particular, estimating the cost of an IaC deployment requires estimating the future usage and pricing models of every cloud resource in the deployment. Gaining transparency into predicted usage/costs is a leading challenge in cloud management. Existing work either relies on historical usage metrics to predict cost or on coarse-grain static analysis that ignores interactions between resources. Our key insight is that the topology of an IaC deployment imposes constraints on the usage of each resource, and we can formalize and automate the reasoning on constraints by using an SMT solver. This allows customers to have formal guarantees on the bounds of their cloud usage. We propose a tool for fine-grained static usage analysis that works by modeling the inter-resource interactions in an IaC deployment as a set of SMT constraints, and evaluate our tool on a benchmark of over 1000 real world IaC configurations. 

Reactive program synthesis from logical specifications has yet to match the user-friendly approach of examplebased programming for spreadsheets, despite its success in specific domains. A main challenge hindering the broader adoption of reactive synthesis is in the complexity of specification engineering in temporal logics. We map out challenges and tools that arise as users write temporal logic specifications in Temporal Stream Logic. Our goal is to provide a roadmap for future usability work that can elevate temporal specification engineering for synthesis to match the usability support available for software engineering. By generalizing these concepts, we can gain a deeper insight into the challenges people face when reasoning about the temporal behavior of their systems. 

MaxMSP is a visual programming language for creating interactive audiovisual media that has found great success as a flexible and accessible option for computer music. However, the visual interface requires manual object placement and connection, which can be inefficient. Automated patch editing is possible either by visual programming with the [thispatcher] object or text-based programming with the [js] object. However, these objects cannot automatically create and save new patches, and they operate at run-time only, requiring live input to trigger patch construction. There is no solution for automated creation of multiple patches at \textitcompile-time, such that the constructed patches do not contain their own constructors. To this end, we present MaxPy, an open-source Python package for programmatic construction and manipulation of MaxMSP patches. MaxPy replaces the manual actions of placing objects, connecting patchcords, and saving patch files with text-based Python functions, thus enabling dynamic, procedural, high-volume patch generation at compile-time. MaxPy also includes the ability to import existing patches, allowing users to move freely between text-based Python programming and visual programming with the Max GUI. MaxPy enables composers, programmers, and creators to explore expanded possibilities for complex, dynamic, and algorithmic patch construction through text-based Python programming of MaxMSP. 

Temporal logic specifications can be used to synthesize reactive systems by writing high-level descriptions of desired behavior, without the need to manually program a complete system. While synthesis from temporal logics has long been focused on hardware systems, recent work has expanded applications of synthesis to include areas of broader interest, such as mobile apps, visualization, and self-driving cars. These new application areas have the potential to bring new types of users into the synthesis community, but significant usability hurdles remain. In this work, we investigate how Temporal Stream Logic (TSL), a temporal logic specification language, can be made more usable and approachable to programmers of all skill levels. We propose a study design to evaluate the usefulness of an alternative interface for writing TSL to address the syntactic hurdle of temporal logic. We then outline areas for improvement and exploration in TSL and reactive synthesis as a whole. 

Hardware IP verification requires collaboration from several parties, including the 3PIP vendor, IP user, and EDA tool vendor, all of whom could threaten the design's integrity and confidentiality. Various frameworks and tools, including the IEEE 1735 standard, have been developed to address these concerns. However, these solutions fall short of the zero trust model's requirements. To overcome this, we propose a novel zero trust formal verification framework that incorporates secure multiparty computation to ensure the privacy of all the parties involved in the verification process. The efficiency of the framework is demonstrated by checking various open-source IP-level benchmarks. 

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic modulo theories (TSL-MT), a framework that unites the two approaches to synthesize a single program. In our approach, reactive synthesis and SyGuS collaborate in the synthesis process, and generate executable code that implements both reactive and data-level properties. We present a tool, temos, that combines state-of-the-art methods in reactive synthesis and SyGuS to synthesize programs from TSL-MT specifications. We demonstrate the applicability of our approach over a set of benchmarks, and present a deep case study on synthesizing a music keyboard synthesizer.