Yongwook Choi

Seunghwan Kim

Kyungho Song

Seojin Kim

Jungyeom Kim

Programming Language Research Group (PLRG) at Korea University. Our research goal is to help developers design and implement high-quality software using diverse programming language technologies. Especially our research interests are as follows: program analysis for automatically understanding program behaviors and detecting bugs and vulnerabilities, mechanized specification to fill the gap between human-readable specifications and machine-friendly software, program synthesis to lessen the burden of software development by automatically generating programs, automated testing to generate test cases for software automatically on behalf of humans.

한국대학교 프로그래밍 언어 연구 그룹 (PLRG). 저희 연구의 목표는 개발자들이 다양한 프로그래밍 언어 기술을 사용하여 고품질 소프트웨어를 설계하고 구현하도록 돕는 것입니다. 특히 저희의 연구 관심사는 다음과 같습니다: 프로그램 동작을 자동으로 이해하고 버그 및 취약점을 탐지하기 위한 프로그램 분석, 사람이 읽을 수 있는 사양과 기계 친화적인 소프트웨어 사이의 간극을 메우기 위한 자동화된 사양, 프로그램을 자동으로 생성하여 소프트웨어 개발의 부담을 덜기 위한 프로그램 합성, 인간을 대신하여 소프트웨어에 대한 테스트 케이스를 자동으로 생성하기 위한 자동화된 테스팅.

Verification and Classification of Exploits for Node.js Vulnerabilities

Debun: Detecting Bundled JavaScript Libraries on Web using Property-Order Graphs

JSSpecVis: A JavaScript Language Specification Visualization Tool

PL4XGL: A Programming Language Approach to Explainable Graph Learning

JavaScript Language Design and Implementation in Tandem

Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations

Automatically Deriving JavaScript Static Analyzers from Specifications using Meta-Level Static Analysis

Filling the Gap between the JavaScript Language Specification and Tools using the JISET Family

A Survey of Parametric Static Analysis

JSTAR: JavaScript Specification Type Analyzer using Refinement

Accelerating JavaScript Static Analysis via Dynamic Shortcuts

JavaScript Static Analysis with Evolving Engines and Specification

JEST: N+1-version Differential Testing of Both JavaScript Engines and Specification

JISET: JavaScript IR-based Semantics Extraction Toolchain

Toward Analysis and Bug Finding of JavaScript Web Applications in the Wild

Path Dependent Types with Path-Equality

A Framework for Dynamic Inter-Device Task Dispatch with Eventual Consistency

Toward Building Memory-safe Network Functions with Modest Performance Overhead

Revisiting Recency Abstraction for JavaScript: Towards an Intuitive, Compositional, and Efficient Heap Abstraction

Analysis of JavaScript Web Applications Using SAFE 2.0

JavaScript API Misuse Detection by Using TypeScript

A survey of parametric static analysis

Analysis of JavaScript web applications using SAFE 2.0

Accelerating JavaScript static analysis via dynamic shortcuts

JavaScript API misuse detection by using typescript

Toward analysis and bug finding in JavaScript web applications in the wild

Automatically deriving JavaScript static analyzers from specifications using Meta-level static analysis

JSTAR: JavaScript specification type analyzer using refinement

Feature-sensitive coverage for conformance testing of programming language implementations

Pl4xgl: A programming language approach to explainable graph learning

Sukyoung Ryu

Joonyoung Park

Jihee Park

Yeonhee Ryou

Xavier Rival

Jaemin Hong

Jihyeok Park

Modern programming follows the continuous integration (CI) and continuous deployment (CD) approach rather than the traditional waterfall model. Even the development of modern programming languages uses the CI/CD approach to swiftly provide new language features and to adapt to new development environments. Unlike in the conventional approach, in the modern CI/CD approach, a language specification is no more the oracle of the language semantics because both the specification and its implementations (interpreters or compilers) can co-evolve. In this setting, both the specification and implementations may have bugs, and guaranteeing their correctness is non-trivial. In this paper, we propose a novel N + 1-version differential testing to resolve the problem. Unlike the traditional differential testing, our approach consists of three steps: (1) to automatically synthesize programs guided by the syntax and …

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 …

Understanding program behaviors is important to verify program properties or to optimize programs. Static analysis is a widely used technique to approximate program behaviors via abstract interpretation. To evaluate the quality of static analysis, researchers have used three metrics: performance, precision, and soundness. The static analysis quality depends on the analysis techniques used, but the best combination of such techniques may be different for different programs. To find the best combination of analysis techniques for specific programs, recent work has proposed parametric static analysis . It considers static analysis as black-box parameterized by analysis parameters , which are techniques that may be configured without analysis details. We formally define the parametric static analysis, and we survey analysis parameters and their parameter selection in the literature. We also discuss open challenges …

JavaScript has been the language for web applications, and the growing prevalence of web environments in various devices makes JavaScript web applications even more ubiquitous. However, because JavaScript and web environments are extremely dynamic, JavaScript web applications are often vulnerable to type-related errors and security attacks. To lessen the problem, researchers have developed various analysis techniques in different analyzers, but such analyzers are not especially aimed for ease of use by analysis developers. In this paper, we present SAFE 2.0, a scalable analysis framework for ECMAScript especially designed as a playground for advanced research in JavaScript web applications. SAFE 2.0 is light-weight, which supports pluggability, extensibility, and debuggability. Demo video: https://youtu.be/ZI_emiRMoxQ.

JavaScript has become one of the most widely used programming languages for web development, server-side programming, and even micro-controllers for IoT. However, its extremely functional and dynamic features degrade the performance and precision of static analysis. Moreover, the variety of built-in functions and host environments requires excessive manual modeling of their behaviors. To alleviate these problems, researchers have proposed various ways to leverage dynamic analysis during JavaScript static analysis. However, they do not fully utilize the high performance of dynamic analysis and often sacrifice the soundness of static analysis. In this paper, we present dynamic shortcuts, a new technique to flexibly switch between abstract and concrete execution during JavaScript static analysis in a sound way. It can significantly improve the analysis performance and precision by using highly-optimized …

Static analysis of JavaScript programs to detect errors in them is a challenging task. Especially when the program imports massive JavaScript libraries such as jQuery and MooTools, analyzing the whole program and the libraries is expensive and extremely declines the analysis efficiency. In this paper, we introduce a novel approach to solve the problem by modularizing the analysis. We separate the analysis of JavaScript libraries by using types extracted from their corresponding specifications in TypeScript and the analysis of JavaScript applications by a static analysis framework. We use DefinitelyTyped, an open-source repository that provides TypeScript declaration files of over 300 popular JavaScript libraries, and we extend SAFE, an open-source analysis framework for JavaScript.

We present our journey to analyze and find bugs in JavaScript web applications in the wild. We describe technical challenges in analyzing them and our solutions to address the challenges via a series of open source analysis frameworks, the scalable analysis framework for ECMAScript (SAFE) family.

JavaScript is one of the most dominant programming languages. However, despite its popularity, it is a challenging task to correctly understand the behaviors of JavaScript programs because of their highly dynamic nature. Researchers have developed various static analyzers that strive to conform to ECMA-262, the standard specification of JavaScript. Unfortunately, all the existing JavaScript static analyzers require manual updates for new language features. This problem has become more critical since 2015 because the JavaScript language itself rapidly evolves with a yearly release cadence and open development process. In this paper, we present JSAVER, the first tool that automatically derives JavaScript static analyzers from language specifications. The main idea of our approach is to extract a definitional interpreter from ECMA-262 and perform a meta-level static analysis with the extracted interpreter. A …

JavaScript is one of the mainstream programming languages for client-side programming, server-side programming, and even embedded systems. Various JavaScript engines developed and maintained in diverse fields must conform to the syntax and semantics described in ECMAScript, the standard specification of JavaScript. Since an incorrect description in ECMAScript can lead to wrong JavaScript engine implementations, checking the correctness of ECMAScript is critical and essential. However, all the specification updates are currently manually reviewed by the Ecma Technical Committee 39 (TC39) without any automated tools. Moreover, in late 2014, the committee announced the yearly release cadence and open development process of ECMAScript to quickly adapt to evolving development environments. Because of such frequent updates, checking the correctness of ECMAScript becomes more labor …

JavaScript is one of the most widely used programming languages. To understand the behaviors of JavaScript programs and to detect possible errors in them, researchers have developed several static analyzers based on the abstract interpretation framework. However, JavaScript provides various language features that are difficult to analyze statically and precisely such as dynamic addition and removal of object properties, first-class property names, and higher-order functions. To alleviate the problem, JavaScript static analyzers often use recency abstraction , which refines address abstraction by distinguishing recent objects from summaries of old objects. We observed that while recency abstraction enables more precise analysis results by allowing strong updates on recent objects, it is not monotone in the sense that it does not preserve the precision relationship between the underlying address abstraction …

The conformance testing of programming language implementations is crucial to support correct and consistent execution environments. Because manually maintaining conformance tests for real-world programming languages is cumbersome and labor-intensive, researchers have presented various ways to make conformance tests effective and efficient. One such approach is to use graph coverage, one of the most widely-used coverage criteria, to generate tests that reach different parts of a mechanized language specification. Since mechanized specifications use functions or inductive definitions to describe the semantics of language features, traditional graph coverage criteria for software work as they are. However, they may not produce high-quality conformance tests because language implementations often have specialized execution paths for different features, even when their semantics descriptions use the …

Proposing a new approach to programming language development.

In this article, we present a new, language-based approach to explainable graph learning. Though graph neural networks (GNNs) have shown impressive performance in various graph learning tasks, they have severe limitations in explainability, hindering their use in decision-critical applications. To address these limitations, several GNN explanation techniques have been proposed using a post-hoc explanation approach providing subgraphs as explanations for classification results. Unfortunately, however, they have two fundamental drawbacks in terms of 1) additional explanation costs and 2) the correctness of the explanations. This paper aims to address these problems by developing a new graph-learning method based on programming language techniques. Our key idea is two-fold: 1) designing a graph description language (GDL) to explain the classification results and 2) developing a new GDL-based …

While the Scala type system provides expressive features like objects with type members, the lack of equality checking between path-dependent types prohibits some programming idioms. One such an example is abstract domain combinators in implementing static analyzers. In this paper, we propose to extend the Scala type system with path-equality, and formalize it as a DOT variant, π DOT, which supports records with type members and elds. We show that π DOT has the normalization property and prove its type soundness.

The Internet of Things (IoT) allows various things like mobile devices and electronic appliances to communicate over network. Inter-device apps can share data between devices and dispatch specific tasks to other devices to utilize their resources. The prevalence of JavaScript web apps that can run anywhere providing any browsers opens the gate to unanticipated interactions between devices. However, the current techniques require developers construct tasks to dispatch statically with strong consistency, and they do not provide any disciplined way to develop inter-device apps. In this paper, we propose IDTD (Inter-Device Task Dispatch), a framework that allows developers to construct and dispatch tasks into multiple devices dynamically with eventual consistency in a systematic manner. We provide a high-level architecture of IDTD, prove the soundness and eventual consistency of the framework, and present its …

For the past few decades network functions have evolved much in variety and complexity. Contributing factors behind are ever-increasing link speeds, novel hardware features, and new network designs (eg, datacenters), just to name a few [4, 6]. In order to deliver high performance in network I/O, network functions rely heavily on low-level memory management. Yet, such memory management is error-prone. Among the Linux CVEs (Common Vulnerabilities and Exposures) for network functionality with CVSS (Common Vulnerability Scoring System) score 7.5 or higher, more than 30% are due to memory management faults: buffer overflow, null pointer dereferences, use-after-free, and double free. Table 1 shows some examples of critical vulnerabilities from memory-related bugs on the kernel’s network stack. Such bugs often lead system crash, systems being compromised, or leakage of secret information. In traditional type-safe languages (eg, ML, Haskell, Scala), memory-safety is preserved by disallowing pointer manipulation; they automatically manage memory resources without explicit malloc ()/free (), restrict accesses beyond memory bound, and have no null pointer dereferences. There are notable projects of implementing network function using type-safe languages [5, 2, 1]. Yet for performance-critical network functions, intermittent execution of a garbage collector incurs unbearable performance penalty. Rust [3], a recently developed language for safe system programming, aims to support memory-safety without garbage collection via its advanced type system. However, the type system restricts programmability; even frequently used data …

Detecting front-end JavaScript libraries in web applications is essential for website profiling, vulnerability detection, and dependency management. However, bundlers like Webpack transpile code in various ways, altering the original directory and code structure, which complicates library detection. While state-of-the-art techniques utilize property pattern-based library detection at runtime, they face two key limitations:(1) they cannot detect libraries inaccessible from the global object, and (2) they have limitations in granular version detection. To address these challenges, we present DEBUN, a scalable technique for detecting JavaScript libraries and their versions using functionlevel fingerprints. Our key insight is that bundlers preserve the property names and execution order of property operations, even after transpilation. To leverage this, we introduce the propertyorder graph (POG), which represents the execution order of property operations within a function body. We evaluate DEBUN on 68 high-traffic websites with 78 front-end JavaScript libraries. Our approach outperforms existing tools, achieving a 91.76% F1-score in library detection (1.39 x higher) and an 79.81% F1-score in version identification with inclusion match (1.36 x higher).

ECMA-262 is the official language specification for JavaScript that defines the language semantics in detail. However, readers often struggle to understand the specification due to the intricate edge cases and lengthy, highly nested explanations. To address this issue, we present JSSpecVis, an interactive web interface visualizing the JavaScript language specification. For an intuitive understanding of edge cases, it provides example programs for each part of the specification with a call-path context selected by readers. In addition, it supports the interactive execution of JavaScript programs on the specification with a new debugging feature called resume and provenance for advanced debugging of JavaScript programs. Using these functionalities, JSSpecVis provides an intuitive learning environment for beginners and a powerful productivity for experts. Our tool is open at https://github.com/ku-plrg/js-spec-vis, and …

PLRG @ Korea University

교수님 소개

박지혁

연구실 소개

연구실 키워드

알럼나이가 간 회사

연구실 지원 방법

대우 조건

연도별 논문 인용수

저널 & 학회 논문 출판 수

연구실 논문 목록

Verification and Classification of Exploits for Node.js Vulnerabilities

Debun: Detecting Bundled JavaScript Libraries on Web using Property-Order Graphs

JSSpecVis: A JavaScript Language Specification Visualization Tool

연구실 보유 특허

대학별 입시끈

우리 연구실 모집

교수님 소개

박지혁

연구실 키워드

알럼나이가 간 회사

연구실 지원 방법

대우 조건

연도별 논문 인용수

저널 & 학회 논문 출판 수

연구실 논문 목록

Verification and Classification of Exploits for Node.js Vulnerabilities

Debun: Detecting Bundled JavaScript Libraries on Web using Property-Order Graphs

JSSpecVis: A JavaScript Language Specification Visualization Tool

연구실 보유 특허

최근 3년간 연구실적 높은 연구실

대학별 입시끈

우리 연구실 모집