Currently, when a security analyst discovers a vulnerability in critical software system, they must navigate a fraught dilemma: immediately disclosing the vulnerability to the public could harm the system’s users; whereas disclosing the vulnerability only to the software’s vendor lets the vendor disregard or deprioritize the security risk, to the detriment of unwittingly-affected users. A compelling recent line of work aims to resolve this by using Zero Knowledge (ZK) protocols that let analysts prove that they know a vulnerability in a program, without revealing the details of the vulnerability or the inputs that exploit it. In principle, this could be achieved by generic ZK techniques. In practice, ZK vulnerability proofs to date have been restricted in scope and expressibility, due to challenges related to generating proof statements that model real-world software at scale and to directly formulating violated properties. This article presents Cheesecloth , a novel proof-statement compiler, which proves practical vulnerabilities in ZK by soundly-but-aggressively preprocessing programs on public inputs, selectively revealing information about executed control segments, and formalizing information leakage using a novel storage-labeling scheme. Cheesecloth ’s practicality is demonstrated by generating ZK proofs of well-known vulnerabilities in (previous versions of) critical software, including the Heartbleed information leakage in OpenSSL, a memory vulnerability in the FFmpeg multimedia encoding framework, a cryptographic implementation bug in the Secure Scuttlebutt decentralised social network, and a denial of service vulnerability in OpenSSL.

Despite decades of contributions to the theoretical foundations of parsing and the many tools available to aid in parser development, many security attacks in the wild still exploit parsers. The issues are myriad—flaws in memory management in contexts lacking memory safety, flaws in syntactic or semantic validation of input, and misinterpretation of hundred-page-plus standards documents. It remains challenging to build and maintain parsers for common, mature data formats. In response to these challenges, we present Daedalus, a new domain-specific language (DSL) and toolchain for writing safe parsers. Daedalus is built around functional-style parser combinators, which suit the rich data dependencies often found in complex data formats. It adds domain-specific constructs for stream manipulation, allowing the natural expression of parsing noncontiguous formats. Balancing between expressivity and domain-specific constructs lends Daedalus specifications simplicity and leaves them amenable to analysis. As a stand-alone DSL, Daedalus is able to generate safe parsers in multiple languages, currently C++ and Haskell. We have implemented 20 data formats with Daedalus, including two large, complex formats—PDF and NITF–and our evaluation shows that Daedalus parsers are concise and performant. Our experience with PDF forms our largest case study. We worked with the PDF Association to build a reference implementation, which was subject to a red-teaming exercise along with a number of other PDF parsers and was the only parser to be found free of defects.

Advances in device technology have led to an era where entire systems can be implemented on a single component, commonly referred to as system-on-chip. With shrinking product life cycles placing severe time to market demands on manufacturers, coupled with their need to quickly change a product's feature set to address evolving customer requirements, programmability will emerge as a corner-stone for all chips implemented in the future. The Internet, communications, consumer electronics, and computing markets are first to take advantage of system-on-chip technology. What are the benefits of programmability to these and other markets and are there potential pitfalls? What architectures and programmability (or reconfigurability) are going to be the likely winners and at what cost? Are these architectures likely to converge or diverge? The panelists will debate the merits of their existing approaches and how they are likely to be shaped in the future.