检索结果-内蒙古大学图书馆

satisfiability modulo Ordering Consistency theory for SC, TSO, and PSO Memory Models

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2023年第1期45卷 6-6页

作者： Fan, Hongyu Sun, Zhihang He, Fei Tsinghua Univ Sch Software Beijing Peoples R China MoE Key Lab Informat Syst Secur Beijing Peoples R China Beijing Natl Res Ctr Informat Sci & Technol Beijing Peoples R China

Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints. In this article, we propose a novel ordering consistency theory for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called Zord, and have conducted extensive experiments on the SV-COMP 2020 ConcurrencySafety benchmarks. Our experimental results show a significant improvement over the state-of-the-art.

关键词： Program verification satisfiability modulo theory weak memory models concurrency

来源：评论

学校读者我要写书评

暂无评论

satisfiability modulo Ordering Consistency theory for Multi-threaded Program Verification 2021

Satisfiability Modulo Ordering Consistency Theory for Multi-...

引用

42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)

作者： He, Fei Sun, Zhihang Fan, Hongyu Tsinghua Univ Sch Software Beijing Peoples R China MoE China Key Lab Informat Syst Secur Beijing Peoples R China Beijing Natl Res Ctr Informat Sci & Technol Beijing Peoples R China

ISBN: (纸本)9781450383912

Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial-order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks;the results show significant promotion of our approach.

关键词： Program verification satisfiability modulo theory memory consistency model concurrency

来源：评论

学校读者我要写书评

暂无评论

Minimal Context-Switching Data Race Detection with Dataflow Tracking

引用

Journal of Computer Science & Technology 2024年第1期39卷 211-226页

作者：郑龙李洋辛杰刘海峰郑然廖小飞金海 National Engineering Research Center for Big Data Technology and System School of Computer Science and Technology Huazhong University of Science and TechnologyWuhan 430074China Services Computing Technology and System Laboratory School of Computer Science and TechnologyHuazhong University of Science and TechnologyWuhan 430074China Cluster and Grid Computing Laboratory School of Computer Science and TechnologyHuazhong University of Science and TechnologyWuhan 430074China

Data race is one of the most important concurrent anomalies in multi-threaded *** con-straint-based techniques are leveraged into race detection,which is able to find all the races that can be found by any oth-er sound race ***,this constraint-based approach has serious limitations on helping programmers analyze and understand data ***,it may report a large number of false positives due to the unrecognized dataflow propa-gation of the ***,it recommends a wide range of thread context switches to schedule the reported race(in-cluding the false one)whenever this race is exposed during the constraint-solving *** ad hoc recommendation imposes too many context switches,which complicates the data race *** address these two limitations in the state-of-the-art constraint-based race detection,this paper proposes DFTracker,an improved constraint-based race detec-tor to recommend each data race with minimal thread context ***,we reduce the false positives by ana-lyzing and tracking the dataflow in the *** this means,DFTracker thus reduces the unnecessary analysis of false race *** further propose a novel algorithm to recommend an effective race schedule with minimal thread con-text switches for each data *** experimental results on the real applications demonstrate that 1)without removing any true data race,DFTracker effectively prunes false positives by 68%in comparison with the state-of-the-art constraint-based race detector;2)DFTracker recommends as low as 2.6-8.3(4.7 on average)thread context switches per data race in the real world,which is 81.6%fewer context switches per data race than the state-of-the-art constraint based race ***,DFTracker can be used as an effective tool to understand the data race for programmers.

关键词： data race satisfiability modulo theory multi-threaded program dynamic detection

来源：评论

学校读者我要写书评

暂无评论

Improved Side Channel Attacks on TRIVIUM, GRAIN-128-AEAD, ACORN-128 v3 and ASCON-128a

引用

DESIGNS CODES AND CRYPTOGRAPHY 2025年第6期93卷 1911-1933页

作者： Sahoo, Soumya Patil, Raghavendra Mondal, Sandip Kumar Sarkar, Santanu Rebeiro, Chester Indian Inst Technol Madras Dept Math Chennai 600036 Tamil Nadu India Indian Inst Technol Madras Dept Comp Sci & Engn Chennai 600036 Tamil Nadu India

Side Channel Attacks (SCA) exploit physical information leakage from devices performing cryptographic operations, posing significant security threats. While SCA has been extensively studied in the context of block ciphers, similar analyses on stream ciphers and constructions like authenticated encryption are less explored. In this paper, we present a novel enhancement to existing SCA techniques based on the hamming weight model for stream ciphers. We have identified critical oversights in previous SCA attack models, allowing us to introduce additional inequalities that enhance the model's effectiveness. For TRIVIUM and GRAIN-128-AEAD, we demonstrate that a practical state recovery attack can be achieved in significantly less time than existing attacks on the HW/32 model. Furthermore, we show that our improved model is capable of handling the HW/64 model and can recover the state even with noisy traces within a few hours. Additionally, we extend our model to the authenticated encryption schemes ACORN-128 v3 and ASCON-128a, demonstrating its broader applicability.

关键词： Stream Cipher TRIVIUM GRAIN-128-AEAD ACORN-128 v3 ASCON-128a Side Channel Attack satisfiability modulo theory

来源：评论

学校读者我要写书评

暂无评论

SMT-Based Repair of Disjunctive Temporal Networks with Uncertainty: Strong and Weak Controllability 1

引用

21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR)

作者： Sumic, Ajdin Cimatti, Alessandro Micheli, Andrea Vidal, Thierry Tech Univ Tarbes LGP ENIT Tarbes France Fdn Bruno Kessler Trento Italy

ISBN: (数字)9783031605994

ISBN: (纸本)9783031606014;9783031605994

Temporal Networks with Uncertainty are a powerful and widely used formalism for representing and reasoning over temporal constraints in the presence of uncertainty. Since their introduction, they have been used in planning and scheduling applications to model situations where some activity durations or event timings are not under the control of the scheduling agent. Moreover, a wide variety of classes of temporal networks (depending on the types of constraints) have been defined, and many algorithms for dealing with these emerged. We are interested in the repair problem, consisting of reconsidering the bounds of the uncertain durations when the network is not controllable, i.e., when no strategy for scheduling exists. This problem is important, as it allows for the explanation and negotiation of the problematic uncertainties. In this paper, we address the repair problem for a very expressive class of temporal networks, namely the Disjunctive Temporal Networks with Uncertainty. We use the satisfiability modulo theory framework to formally encode and solve the problem, and we devise a uniform solution encompassing different "levels" of controllability, namely strong and weak. Moreover, we provide specialized encodings for important sub-classes of the problem, and we experimentally evaluate our approaches.

关键词： Disjunctive Temporal Network with Uncertainty Plan Repair satisfiability modulo theory Strong and Weak Controllability

来源：评论

学校读者我要写书评

暂无评论

Using linear algebra in decomposition of Farkas interpolants

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2022年第1期24卷 111-125页

作者： Blicha, Martin Hyvarinen, Antti E. J. Kofron, Jan Sharygina, Natasha Univ Svizzera Italiana USI Lugano Switzerland Charles Univ Prague Fac Math & Phys Prague Czech Republic

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas' lemma. However, these interpolants do not always suit the verification task-in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

关键词： Model checking satisfiability modulo theory Linear real arithmetic Craig interpolation

来源：评论

学校读者我要写书评

暂无评论

SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study 1

引用

24th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) part of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)

作者： Banerjee, Soham Ghosh, Sumana Banerjee, Ansuman Mohalik, Swarup K. Indian Stat Inst Kolkata India Ericsson Res Bangalore Karnataka India

ISBN: (数字)9783031249501

ISBN: (纸本)9783031249495;9783031249501

In this paper, we present a case study on modeling and verification of Spiking Neural Networks (SNN) using satisfiability modulo theory (SMT) solvers. SNN are special neural networks that have great similarity in their architecture and operation with the human brain. These networks have shown similar performance when compared to traditional networks with comparatively lesser energy requirement. We discuss different properties of SNNs and their functioning. We then use Z3, a popular SMT solver to encode the network and its properties. Specifically, we use the theory of Linear Real Arithmetic (LRA). Finally, we present a framework for verification and adversarial robustness analysis and demonstrate it on the Iris and MNIST benchmarks.

关键词： Spiking neural networks satisfiability modulo theory Verification Adversarial robustness

来源：评论

学校读者我要写书评

暂无评论

Verifying Neural Networks with Non-Linear SMT Solvers: a Short Status Report 35

Verifying Neural Networks with Non-Linear SMT Solvers: a Sho...

引用

35th IEEE International Conference on Tools with Artificial Intelligence (ICTAI)

作者： Guidotti, Dario Pandolfo, Laura Pulina, Luca Univ Sassari DUMAS Sassari Italy

ISBN: (纸本)9798350342734

In the last couple of decades, the popularity of neural networks has soared and they have been successfully utilized in many different domains across computer science. However, their application in safety and security-critical domains has been limited due to concerns regarding their reliability. Traditional methods for verifying neural networks (NNs) often uses linear satisfiability modulo theory (SMT) solvers. These solvers work well for simple and shallow NN architectures but face limitations regarding their inability to handle non-linear activations, pooling layers, and complex activation functions, commonly used in modern deep neural networks. In this paper, we explore the potential of non-linear SMT solvers to verify intricate neural network architectures. By leveraging non-linear SMT solvers, a wider range of activation functions can be considered, leading to more accurate reasoning about the behavior of complex deep neural networks. The focus is on using recent advancements in SMT solver development to verify NNs with non-linear activation functions, particularly in the context of Computer Vision tasks. To test this idea, we conducted an experimental analysis to assess whether current non-linear SMT solvers can efficiently handle NNs with transcendent activation functions.

关键词： Trustworthy AI Formal Verification Neural Networks satisfiability modulo theory

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of Neural Network Controllers for Collision-Free Flight 13th

Formal Verification of Neural Network Controllers for Collis...

引用

14th International Workshop on Numerical Software Verification (NSV)

作者： Genin, Daniel Papusha, Ivan Brule, Joshua Young, Tyler Mullins, Galen Kouskoulas, Yanni Wu, Rosa Schmidt, Aurora Johns Hopkins Univ Appl Phys Lab 11100 Johns Hopkins Rd Laurel MD 20723 USA Def Nucl Facil Safety Board Washington DC USA

ISBN: (纸本)9783030955618;9783030955601

We investigate a method for formally verifying the absence of adversarial examples in a neural network controller. Our approach applies to networks with piecewise affine activation units, which may be encoded symbolically as a piecewise affine mapping from inputs to outputs. The approach rests on characterizing and bounding a critical subset of the state space where controller action is required, partitioning this critical subset, and using satisfiability modulo theories (SMT) to prove nonexistence of safety counterexamples on each of the resulting partition elements. We demonstrate this approach on a simple collision avoidance neural network controller, trained with reinforcement learning to avoid collisions in a simplified simulated environment. After encoding the network weights in SMT, we formally verify safety of the neural network controller on a subset of the critical partition elements, and determine that the rest of the critical set partition elements are potentially unsafe. We further experimentally confirm the existence of actual adversarial collision scenarios in 90% of the identified potentially unsafe critical partition elements, indicating that our approach is reasonably tight.

关键词： Reinforcement learning satisfiability modulo theory Formal verification

来源：评论

学校读者我要写书评

暂无评论

Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification 22

Interference Relation-Guided SMT Solving for Multi-Threaded ...

引用

27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)

作者： Fan, Hongyu Liu, Weiting He, Fei Tsinghua Univ Sch Software Key Lab Informat Syst Secur MoE Beijing Natl Res Ctr Informat Sci & Technol Beijing Peoples R China

ISBN: (纸本)9781450392044

Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing works, an SMT solver is simply treated as the backend. There is little research on improving SMT solving for concurrent program verification. In this paper, we recognize the characteristics of interference relation in multi-threaded programs and propose a novel approach for utilizing the interference relation in the SMT solving of multi-threaded program verification under various memory models. We show that the backend SMT solver can benefit a lot from the domain knowledge of concurrent programs. We implemented our approach in a prototype tool called ZPRE. We compared it with the state-of-the-art Z3 tool on credible benchmarks from the ConcurrencySafety category of SV-COMP 2019. Experimental results show promising improvements attributed to our approach.

关键词： Concurrent programs Program verification satisfiability modulo theory Partial order Weak memory models

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：