JaVerT: a JavaScript Verification Toolchain

Abstract: The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. In this talk, I will describe JaVerT, a semi-automatic JavaScript Verification Toolchain based on separation logic. JaVerT is aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. The specification challenge is to […]

Read More

Tree-Sitter: A New Parsing System for Programming Tools

Abstract: Developer tools that support multiple languages generally have very limited regex-based code-analysis capabilities. Tree-sitter is a new parsing system that aims to change this paradigm. We’re in the process of integrating Tree-sitter into both GitHub.com and Atom, which will allow us to analyze code accurately and in real-time, paving the way for better syntax […]

Read More

An Update on the Habit Programming Language

Abstract: Habit is a high-level programming language, originally based on Haskell, that was designed to meet the needs of high assurance, very low-level software development. The most recent version of the language report was completed in 2010, and an initial working prototype implementation was developed by the HASP group at PSU. However, there has not […]

Read More

RustBelt: Securing the Foundations of the Rust Programming Language

Abstract: Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power […]

Read More

RustBelt: Securing the Foundations of the Rust Programming Language

Abstract: Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power […]

Read More

Robust Artificial Intelligence and Anomaly Detection

Abstract: Recent progress in AI and machine learning is stimulating interest in applying AI in high stakes applications such as self-driving cars, surgical robots, and autonomous weapons systems. These applications require high levels of software assurance and resilience, but virtually all AI research has focused on raw performance without paying attention to questions of robustness […]

Read More

Datatype Generic Packet Descriptions

Abstract: Complex protocols describing the communication or storage of binary data are difficult to describe precisely. In this talk, I want to explore how to define data types describing a binary data formats and generate the corresponding serialization and deserialization functions from such descriptions. By embedding these data types in a general purpose dependently typed […]

Read More

Rust: from POPL to practice

Abstract: In 2015, a language based fundamentally on substructural typing–Rust–hit its 1.0 release, and less than a year later it has been put into production use in a number of tech companies, including some household names. The language has started a trend, with several other mainstream languages, including C++ and Swift, in the early stages […]

Read More

Tech Talk: E3DB – Tozny’s End-to-End Encrypted Database

abstract: Project E3DB is a tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. We are providing a command-line client for you to play with and a Java SDK to prototype with. Over the next few weeks, we’ll be getting feedback from you, adding features, and making it […]

Read More

Tech talk: Verified Secure Computing using Trusted Hardware

abstract: Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code […]

Read More