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

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

来源：评论

学校读者我要写书评

暂无评论

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

引用

DESIGNS CODES AND CRYPTOGRAPHY 2025年 1-23页

作者： 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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

SMT-based query tracking for differentially private data analytics systems

引用

Frontiers of Computer Science 2018年第6期12卷 1192-1207页

作者： Chen LUO Fei HE Tsinghua National Laboratory for Information Science and Technology (TNList) School of SoftwareTsinghua UniversityBeijing 100084China Key Laboratory for Information System Security Ministry of EducationTsinghua UniversityBeijing 100084China

Differential privacy enables sensitive data to be analyzed in a privacy-preserving manner. In this paper, we focus on the online setting where each analyst is assigned a privacy budget and queries the data interactively. However, existing differentially private data analytics systems such as PINQ process each query independently, which may cause an unnecessary waste of the privacy budget. Motivated by this, we present a satisfiability modulo theories (SMT)-based query tracking approach to reduce the privacy budget usage. In brief, our approach automatically locates past queries that access disjoint parts of the dataset with respect to the current query to save the privacy cost using the SMT solving techniques. To improve efficiency, we further propose an optimization based on explicitly specified column ranges to facilitate the search process. We have implemented a prototype of our approach with Z3, and conducted several sets of experiments. The results show our approach can save a considerable amount of the privacy budget and each query can be tracked efficiently within milliseconds.

关键词： differential privacy privacy budget satisfiability modulo theory

来源：评论

学校读者我要写书评

暂无评论

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers

引用

JOURNAL OF AUTOMATED REASONING 2016年第4期56卷 387-457页

作者： Dross, Claire Conchon, Sylvain Kanig, Johannes Paskevich, Andrei Univ Paris 11 CNRS LRI F-91405 Orsay France INRIA Saclay Ile de France Toccata F-91893 Orsay France AdaCore F-75009 Paris France

satisfiability modulo theories (SMT) solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL modulo theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists and sets.

关键词： Automated deduction satisfiability modulo theory Decision procedures

来源：评论

学校读者我要写书评

暂无评论

Leveraging Control Flow Knowledge in SMT Solving of Program Verification

引用

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 2021年第4期30卷 p1-26页

作者： Chen, Jianhui 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

satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.

关键词： Program verification satisfiability modulo theory control-flow graph

来源：评论

学校读者我要写书评

暂无评论

Assessing SMT and CLP approaches for workflow nets verification

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2018年第4期20卷 467-491页

作者： Bride, Hadrien Kouchnarenko, Olga Peureux, Fabien Voiron, Guillaume Univ Bourgogne Franche Comte Inst FEMTO ST UMR CNRS 6174 16Route Gray F-25030 Besancon France Ecole Cent Nantes LS2N UMR CNRS 6004 1 Rue No F-44300 Nantes France

In the actual business world, companies rely more and more on workflows to model the core of their business processes. In this context, the focus of workflow analysts is made on the verification of workflows specifications, in particular of modal specifications that allow the description of necessary or admissible behaviors. The design and the analysis of business processes commonly relies on workflow nets, a suited class of Petri nets. The goal of this paper is to evaluate and compare in a deep way two resolution methods-satisfiability modulo theory and constraint logic programming-applied to the verification of modal specifications over workflow nets. Firstly, it provides a concise description of the verification methods based on constraint solving. Secondly, it introduces the toolchain developed to automate the full verification process. Thirdly, it describes the experimental protocol designed to evaluate and compare the scalability and efficiency of both resolution approaches and reports on the obtained results. Finally, these obtained results are discussed in detail, lessons learned from these experiments are given, and, on the basis of experiments feedback, directions for improvement and future work are suggested.

关键词： Workflow nets Modal specifications Verification method Experimental comparison satisfiability modulo theory Constraint solving problem

来源：评论

学校读者我要写书评

暂无评论

Time-Triggered Co-Scheduling of Computation and Communication with Jitter Requirements

引用

IEEE TRANSACTIONS ON COMPUTERS 2018年第1期67卷 115-129页

作者： Minaeva, Anna Akesson, Benny Hanzalek, Zdenek Dasari, Dakshina Czech Tech Univ Fac Elect Engn Prague 16636 Czech Republic Czech Tech Univ Czech Inst Informat Robot & Cybernet Prague 16636 Czech Republic CISTER INESC TEC P-4249015 Oporto Portugal ISEP P-4249015 Oporto Portugal Robert Bosch GmbH Corp Res D-71272 Renningen Germany

The complexity of embedded application design is increasing with growing user demands. In particular, automotive embedded systems are highly complex in nature, and their functionality is realized by a set of periodic tasks. These tasks may have hard real-time requirements and communicate over an interconnect. The problemis to efficiently co-schedule task execution on cores and message transmission on the interconnect so that timing constraints are satisfied. Contemporary works typically deal with zero-jitter scheduling, which results in lower resource utilization, but has lower memory requirements. This article focuses on jitter-constrained scheduling that puts constraints on the tasks jitter, increasing schedulability over zero-jitter scheduling. The contributions of this article are: 1) Integer Linear Programming and satisfiability modulo theory model exploiting problem-specific information to reduce the formulations complexity to schedule small applications. 2) A heuristic approach, employing three levels of scheduling scaling to real-world use-cases with 10,000 tasks and messages. 3) An experimental evaluation of the proposed approaches on a case-study and on synthetic data sets showing the efficiency of both zero-jitter and jitter-constrained scheduling. It shows that up to 28 percent higher resource utilization can be achieved by having up to 10 times longer computation time with relaxed jitter requirements.

关键词： Real-time systems automotive systems resource scheduling jitter control integer linear programming satisfiability modulo theory

来源：评论

学校读者我要写书评

暂无评论

Symbolic computation of differential equivalences

引用

THEORETICAL COMPUTER SCIENCE 2019年 777卷 132-154页

作者： Cardelli, Luca Tribastone, Mirco Tschaikowski, Max Vandin, Andrea Univ Oxford Oxford England IMT Sch Adv Studies Lucca Lucca Italy Vienna Univ Technol Vienna Austria Tech Univ Denmark DTU Compute Lyngby Denmark

Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs. We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. We provide novel symbolic procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories. We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii) bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. Using ERODE, the tool that implements our techniques, we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques. (C) 2019 Elsevier B.V. All rights reserved.

关键词： Quantitative equivalence relations satisfiability modulo theory Ordinary differential equations Partition refinement

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：