Kyungmin Bae

Pohang University of Science and Technology

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Peter Csaba Ölveczky

University of Oslo

José Meseguer

University of Illinois Urbana-Champaign

Jaime Arias

Laboratoire d'Informatique de Paris-Nord

Carlos Olarte

Laboratoire d'Informatique de Paris-Nord

Jaehun Lee

Pohang University of Science and Technology

Laure Petrucci

Laboratoire d'Informatique de Paris-Nord

Geunyeol Yu

Pohang University of Science and Technology

Fredrik Rømming

University of Cambridge

Sicun Gao

University of California, San Diego

Sharon Kim

Columbia University

Cooperative Institutions

Pohang University of Science and Technology

Korea Post

Centre National de la Recherche Scientifique

Universidad Politécnica de Madrid

University of Illinois Urbana-Champaign

Laboratoire d'Informatique de Paris-Nord

Carnegie Mellon University

SRI International

Télécom Paris

Universitat Politècnica de València

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Formal Specification and Model Checking of TLS Software Security Requirements using Maude

Journal of KIISE (2024)

Jaehun Lee Kyungmin Bae

TLS(Transport Layer Security) 프로토콜은 컴퓨터 네트워크 상에서 암호화된 통신 기능을 제공하는 프로토콜로 HTTPS, 이메일, VolP 등 다양한 네트워크 애플리케이션에서 널리 사용되고 있다. TLS와 같은 보안 프로토콜의 오류는 많은 보안 취약점을 야기하기 때문에 이의 엄밀한 검증은 매우 중요한 문제이다. 따라서 프로토콜의 스펙 수준에서 보안성 성질을 검증하기 위한 여러 모델검증 기술이 연구되어 왔다. 하지만 프로토콜 스펙 수준에서의 검증은 설계 수준에서 발생하는 오류들을 탐지하지 못하는 한계점이 존재한다. 본 논문에서는 TLS 소프트웨어를 Maude 프레임워크를 사용하여 설계 수준에서 정형명세하고, 이를 통하여 FREAK 공격과 같이 설계 수준에서 발생하는 취약점을 모델검증을 이용하여 엄밀하게 분석할 수 있음을 보였다.

10.5626/jok.2024.51.5.426

Cite

Citations (0)

MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-physical Systems

ACM Transactions on Embedded Computing Systems (2021)

Kyungmin Bae Peter Csaba Ölveczky

TTA and PALS are two prominent formal design patterns—with different strengths and weaknesses—for virtually synchronous distributed cyber-physical systems (CPSs). They greatly simplify the design and verification of such systems by allowing us to design and verify their underlying synchronous designs. In this paper we introduce and verify MSYNC as a formal design (and verification) pattern/synchronizer for hierarchical multirate CPSs that generalizes, and combines the advantages of, both TTA and (single-rate and multirate) PALS. We also define an extension of TTA to multirate CPSs as a special case. We show that MSYNC outperforms both TTA and PALS in terms of allowing shorter periods, and illustrate the MSYNC design and verification approach with a case study on a fault-tolerant distributed control system for turning an airplane.

Synchronizer

Cyber-physical system

Strengths and weaknesses

10.1145/3477036

Cite

Citations (4)

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving

arXiv (Cornell University) (2023)

Jaime Arias Kyungmin Bae Carlos Olarte Peter Csaba Ölveczky Laure Petrucci

Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Roméo can be done in Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments on three benchmarks show that our methods outperform Roméo in many cases.

10.48550/arxiv.2303.08929

Cite

Citations (1)

Formal Patterns for Multi-rate Distributed Real-Time Systems

Lecture notes in computer science (2013)

Kyungmin Bae José Meseguer Peter Csaba Ölveczky

Asynchrony (computer programming)

Aileron

Hierarchical control system

10.1007/978-3-642-35861-6_1

Cite

Citations (9)

A Rewriting-logic-with-SMT-based Formal Analysis and Parameter Synthesis Framework for Parametric Time Petri Nets

Fundamenta Informaticae (2024)

Jaime Arias Kyungmin Bae Carlos Olarte Peter Csaba Ölveczky Laure Petrucci

This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the “standard” semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude—including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking—for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Roméo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Roméo in many cases.

10.3233/fi-242195

Cite

Citations (0)

SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems

Kyungmin Bae Peter Csaba Ölveczky Soonho Kong Sicun Gao Edmund M. Clarke

This paper presents general techniques for verifying virtually synchronous distributed control systems with interconnected physical environments. Such cyber-physical systems (CPSs) are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. To simplify their analysis, we first extend the PALS methodology---that allows to abstract from the timing of events, asynchronous communication, network delays, and imprecise clocks, as long as the infrastructure guarantees bounds on the network delays and clock skews---from real-time to hybrid systems. We prove a bisimulation equivalence between Hybrid PALS synchronous and asynchronous models. We then show how various verification problems for synchronous Hybrid PALS models can be reduced to SMT solving over nonlinear theories of the real numbers. We illustrate the Hybrid PALS modeling and verification methodology on a number of CPSs, including a control system for turning an airplane.

Bisimulation

Cyber-physical system

10.1145/2883817.2883849

Cite

Citations (15)

Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving

Science of Computer Programming (2023)

Jaime Arias Kyungmin Bae Carlos Olarte Peter Csaba Ölveczky Laure Petrucci

Timed automaton

10.1016/j.scico.2023.103074

Cite

Citations (2)

SMT Encoding of Hybrid Systems in dReal

EPiC series in computing (2018)

Kyungmin Bae Soonho Kong Sicun Gao

Analysis problems of hybrid systems, involving nonlinear real functions and ordinary differential equations, can be reduced to SMT (satisfiability modulo theories) problems over the real numbers. The dReal solver can automatically check the satisfiability of such SMT formulas up to a given precision δ > 0. This paper explains how bounded model checking problems of hybrid systems are encoded in dReal. In particular, a novel SMT syntax of dReal enables to effectively represent networks of hybrid systems in a modular way. We illustrate SMT encoding in dReal with simple nonlinear hybrid systems.

Satisfiability Modulo Theories

Satisfiability

Solver

Boolean satisfiability problem

10.29007/s3b9

Cite

Citations (2)

SMT-based Formal Verification Methods of Deep Neural Networks using Structural Properties

Journal of KIISE (2021)

Moonhyeon Chung Kyungmin Bae

심층신경망(Deep neural network, DNN)은 음성 인식, 이미지 분류 등의 다양한 분야에서 소프트웨어를 위하여 널리 활용되고 있다. 하지만 DNN에는 적대적 예제와 같은 예상치 못한 오류가 존재할 수 있으며, 이를 방지하기 위하여 DNN의 요구사항을 검증하기 위한 DNN 정형검증 기술이 활발하게 연구되고 있다. 본 논문에서는 DNN의 요구사항 검증의 성능을 향상하기 위하여 DNN의 구조적 성질을 활용하는 방법론을 제안한다. 본 논문에서는 DNN의 구조적 성질을 수학적으로 정의하고, ReLU를 활성함수로 가지는 DNN의 두 가지 구조적 성질을 제안하였으며 이를 이용하여 SMT 기반 DNN 검증의 성능을 향상시킬 수 있음을 보였다.

Deep Neural Networks

10.5626/jok.2021.48.9.998

Cite

Citations (0)

Modular SMT-based analysis of nonlinear hybrid systems

Kyungmin Bae Sicun Gao

We present SMT-based techniques for analyzing networks of nonlinear hybrid systems, which interact with each other in both discrete and continuous ways. We propose a modular encoding method to reduce reachability problems of hybrid components, involving continuous I/O as well as usual discrete I/O, into the satisfiability of first-order logic formulas over the real numbers. We identify a generic class of logical formulas to modularly encode networks of hybrid systems, and present an SMT algorithm for checking the satisfiability of such logical formulas. The experimental results show that our techniques significantly increase the performance of SMT-based analysis for networks of nonlinear hybrid components.

Satisfiability

ENCODE

Satisfiability Modulo Theories

10.23919/fmcad.2017.8102258

Cite

Citations (9)