Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains.

In this work we present just-in-time synthesis (JITS) for GR(1). Rather than constructing a controller at synthesis time, we compute next states during system execution, and only when they are required. We prove that JITS does not compromise the correctness of the synthesized system execution. We further show that the basic algorithm can be extended to enable several variants.

We have implemented JITS in the Spectra synthesizer. Our evaluation, comparing JITS to existing tools over known benchmark specifications, shows that JITS reduces (1) total synthesis time, (2) the size of the synthesis output, and (3) the loading time for system execution, all while having little to no effect on system execution performance.

Shahar Maoz

Tel Aviv University, Israel

Israel

Ilia Shevrin

Tel Aviv University

JavaScript was initially designed for client-side programming in web browsers, but its engine is now embedded in various kinds of host software. Despite the popularity, since the JavaScript semantics is complex especially due to its dynamic nature, understanding and reasoning about JavaScript programs are challenging tasks. Thus, researchers have proposed several attempts to define the formal semantics of JavaScript based on ECMAScript, the official JavaScript specification. However, the existing approaches are manual, labor-intensive, and error-prone and all of their formal semantics target ECMAScript 5.1 (ES5.1, 2011) or its former versions. Therefore, they are not suitable for understanding modern JavaScript language features introduced since ECMAScript 6 (ES6, 2015). Moreover, ECMAScript has been annually updated since ES6, which already made five releases after ES5.1. To alleviate the problem, we propose JISET, a JavaScript IR-based Semantics Extraction Toolchain. It is the first tool that automatically synthesizes parsers and AST-IR translators directly from a given language specification, ECMAScript. For syntax, we develop a parser generation technique with lookahead parsing for BNFES, a variant of the extended BNF used in ECMAScript. For semantics, JISET synthesizes AST-IR translators using forward compatible rule-based compilation. Compile rules describe how to convert each step of abstract algorithms written in a structured natural language into IRES, an Intermediate Representation that we designed for ECMAScript. For the four most recent ECMAScript versions, JISET automatically synthesized parsers for all versions, and compiled 95.03% of the algorithm steps on average. After we complete the missing parts manually, the extracted core semantics of the latest ECMAScript (ES10, 2019) passed all 18,064 applicable tests. Using this first formal semantics of modern JavaScript, we found nine specification errors in ES10, which were all confirmed by the Ecma Technical Committee 39. Furthermore, we showed that JISET is forward compatible by applying it to nine feature proposals ready for inclusion in the next ECMAScript, which let us find four errors in the BigInt proposal.

Jihyeok Park

KAIST, South Korea

South Korea

Jihee Park

KAIST

South Korea

Seungmin An

KAIST

Sukyoung Ryu

KAIST

South Korea

Regular expressions (regexes) are widely used in different fields of computer science such as programming languages, string processing and databases. However, existing tools for synthesizing or repairing regexes were not designed to be resilient to Regex Denial of Service (ReDoS) attacks. Specifically, if a regex has super-linear (SL) worst-case complexity, an attacker could provide carefully-crafted inputs to launch ReDoS attacks. Therefore, in this paper, we propose a programming-by-example framework, FlashRegex, for generating anti-ReDoS regexes by either synthesizing or repairing from given examples. It is the first framework that integrates regex synthesis and repair with the awareness of ReDoS-vulnerabilities.We present novel algorithms to deduce anti-ReDoS regexes by reducing the ambiguity of these regexes and by using Boolean Satisfiability (SAT) or Neighborhood Search (NS) techniques. We evaluate FlashRegex with five related state-of-the-art tools. The evaluation results show that our work can effectively and efficiently generate anti-ReDoS regexes from given examples, and also reveal that existing synthesis and repair tools have neglected ReDoS-vulnerabilities of regexes. Specifically, the existing synthesis and repair tools generated up to 394 ReDoS-vulnerable regex within few seconds to more than one hours, while FlashRegex generated no SL regex within around five seconds. Furthermore, the evaluation results on ReDoS-vulnerable regex repair also show that FlashRegex has better capability than existing repair tools and even human experts, achieving 4 more ReDoS-invulnerable regex after repair without trimming and resorting, highlighting the usefulness of FlashRegex in terms of generality, automation and user-friendliness.

Yeting Li

Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Zhiwu Xu

Shenzhen University

Jialun Cao

Department of Computer Science and Engineering, The Hong Kong University of Science and Technology

Haiming Chen

Institute of Software, Chinese Academy of Sciences

Tingjian Ge

University of Massachusetts, Lowell

Shing-Chi Cheung

Hong Kong University of Science and Technology, China

China

Haoren Zhao

Shaanxi Normal University, Xi'an, China