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

Ivannikov ISPras Open Conference (ISPras)

作者： Darya Parygina Timofey Mezhuev Daniil Kuts Ivannikov Institute for System Programming of the RAS Moscow Russia Lomonosov Moscow State University Moscow Russia

ISBN: (数字)9798331526023

ISBN: (纸本)9798331526030

Directed fuzzing performs best for targeted program testing via estimating the impact of each input in reaching predefined program points. But due to insufficient analysis of the program structure and lack of flexibility and configurability it can lose efficiency. In this paper, we enhance directed fuzzing with context weights for graph nodes and resolve indirect edges during call graph construction. We construct flexible tool for directed fuzzing with components able to be easily combined with other techniques. We implement proposed method in three separate modules: DiFuzzLLVM library for graph construction and indirect calls resolving, DiFuzz static analysis tool for processing program graphs and computing proximity metrics, and LibAFL-DiFuzz directed fuzzer based on LibAFL fuzzing library. We create additional LibAFL modules for enabling custom power scheduling and static instrumentation. We evaluate indirect calls resolving and get increase in directed fuzzing efficiency for reaching deeper target points. We evaluate context weights contribution and get benefits in TTE and scheduling iterations number. We evaluate our fuzzer in comparison with AFLGo and BEACON, and reveal speedup in time to exposure on several benchmarks. Furthermore, our tool implements some important usability features that are not available in mentioned tools: target points detection, multiple target points support, etc.

关键词： Measurement Processor scheduling Instruments Image edge detection Prototypes Static analysis Fuzzing Libraries Service-oriented architecture Usability

来源：评论

学校读者我要写书评

暂无评论

Verifying cryptographic protocols by Tamarin Prover

Verifying cryptographic protocols by Tamarin Prover

引用

Ivannikov Memorial Workshop (IVMEM)

作者： Evgenii Vinarskii Alexey Demakov Alexander Kamkin Nina Yevtushenko Lomonosov Moscow State University Moscow Russia Ivannikov Institute for System Programming of the RAS Moscow Russia Ivannikov Institute for System Programming of the RAS Moscow Institute of Physics and Technology Higher School of Economics Moscow Russia Higher School of Economics Moscow Russia

ISBN: (数字)9781728190884

ISBN: (纸本)9781728190891

Cryptographic protocols are utilized for establishing a secure session between “honest” agents which communicate strictly according to the protocol rules as well as for ensuring the authenticated and confidential transmission of messages. The specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages including the format of such messages. Note that protocol can describe several execution scenarios. All these requirements lead to a huge formal specification for a real cryptographic protocol and therefore, it is difficult to verify the security of the whole cryptographic protocol at once. In this paper, to overcome this problem, we suggest verifying the protocol security for its fragments. Namely, we verify the security properties for a special set of so-called traces of the cryptographic protocol. Intuitively, a trace of the cryptographic protocol is a sequence of computations, value checks, and transmissions on the sides of “honest” agents permitted by the protocol. In order to choose such set of traces, we introduce an Adversary model and the notion of a similarity relation for traces. We then verify the security properties of selected traces with Tamarin Prover. Experimental results for the EAP and Noise protocols clearly show that this approach can be promising for automatic verification of large protocols.

关键词： Planing Computational modeling Complexity theory Security Formal specifications Cryptography Cryptographic protocols

来源：评论

学校读者我要写书评

暂无评论

A Comprehensive Approach to Finding Resource Leaks via Static Analysis

A Comprehensive Approach to Finding Resource Leaks via Stati...

引用

Ivannikov ISPras Open Conference (ISPras)

作者： Nikita Malyshev Alexey Borodin Andrey Belevantsev Ivannikov Institute for System Programming of the RAS Moscow Russia Lomonosov Moscow State University Moscow Russia

ISBN: (数字)9798331526023

ISBN: (纸本)9798331526030

In the last 15 years many dedicated leak detection tools utilizing novel approaches were designed. Unfortunately, most of them are hard to implement and fully utilize in the scope of a multi-purpose industrial analyzer. In this paper we present a full-fledged approach to static analysis through the lens of resource leak detection. We show how general analysis architecture without much of a focus for specific defects can still be effective at finding leaks both in terms of performance and number of warnings. We briefly describe an overall structure of the Svace static analyzer and how it achieves context and path sensitivities as well as interprocedurality, while allowing for checking many program properties and being highly extensible. We also show how to use this system to implement leak detection algorithm with including a few unique extensions that we have never seen in other instruments. Our test results show a low false positive rate, relatively good performance for a multi-detector static analyzer and great scalability potential both in terms of adding new algorithms and analyzing millions of lines of code.

关键词： Codes Sensitivity Instruments Source coding Scalability Merging Memory management Static analysis Libraries Leak detection

来源：评论

学校读者我要写书评

暂无评论

A Survey of Open-source Tools for FPGA-based Inference of Artificial Neural Networks

A Survey of Open-source Tools for FPGA-based Inference of Ar...

引用

Ivannikov Memorial Workshop (IVMEM)

作者： Mikhail Lebedev Pavel Belecky Plekhanov Russian University of Economics Moscow Russia Ivannikov Institute for System Programming of the RAS Moscow Russia

ISBN: (纸本)9781665423281

During the recent years artificial neural networks have become a great part of everyday life. One of the big problems in AI is acceleration of neural network inference using different hardware: from CPUs and GPUs to FPGAs and ASICs. Many open-source tools have been proposed for this purpose. This article contains a review of a range of open-source tools for neural network optimization, acceleration and hardware synthesis. Tools of three types have been chosen for evaluation: 1) translating neural network models into synthesizable C; 2) accelerating neural network models using custom hardware accelerators; 3) synthesizing Verilog from neural network models. Some of the tools have been tested using five simple neural network examples. Intel CPU, NVIDIA GPU and Cyclone V FPGA hardware platforms have been used for evaluation. Results show that the tested tools can successfully process neural network models and optimize them for CPU and GPU execution, whereas FPGA execution results are controversial.

关键词： Conferences Graphics processing units Artificial neural networks Cyclones Artificial intelligence Hardware design languages Field programmable gate arrays

来源：评论

学校读者我要写书评

暂无评论

Static Analysis for Go: Build Interception

Static Analysis for Go: Build Interception

引用

Ivannikov ISPras Open Conference (ISPras)

作者： Varvara Dvortsova Alexey Izbyshev Alexey Borodin Andrey Belevantsev Ivannikov Institute for System Programming of the RAS Moscow Russia Lomonosov Moscow State University Moscow Russia

This paper presents a method for build interception of Go projects and utilizing the intercepted information for building an intermediate representation used in a static analyzer. The paper discusses two approaches: handling invocations of the higher-level go build command and handling invocations of the lower-level compile tool. The second solution is applicable not only to the built-in Go build system but also to other build systems that directly utilize the low-level compile tool, such as Bazel, Please, Pants. It also covers compilations involving CGO.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Sydr-Fuzz: Continuous Hybrid Fuzzing and Dynamic Analysis for Security Development Lifecycle

Sydr-Fuzz: Continuous Hybrid Fuzzing and Dynamic Analysis fo...

引用

Ivannikov ISPras Open Conference (ISPras)

作者： Alexey Vishnyakov Daniil Kuts Vlada Logunova Darya Parygina Eli Kobrin Georgy Savidov Andrey Fedotov Ivannikov Institute for System Programming of the RAS Moscow Institute of Physics and Technology Moscow Russia Lomonosov Moscow State University

Nowadays automated dynamic analysis frameworks for continuous testing are in high demand to ensure software safety and satisfy the security development lifecycle (SDL) requirements. The security bug hunting efficiency of cutting-edge hybrid fuzzing techniques outperforms widely utilized coverage-guided fuzzing. We propose an enhanced dynamic analysis pipeline to leverage productivity of automated bug detection based on hybrid fuzzing. We implement the proposed pipeline in the continuous fuzzing toolset Sydr-Fuzz which is powered by hybrid fuzzing orchestrator, integrating our DSE tool Sydr with libFuzzer and AFL++. Sydr-Fuzz also incorporates security predicate checkers, crash triaging tool Casr, and utilities for corpus minimization and coverage gathering. The benchmarking of our hybrid fuzzer against alternative state-of-the-art solutions demonstrates its superiority over coverage-guided fuzzers while remaining on the same level with advanced hybrid fuzzers. Furthermore, we approve the relevance of our approach by discovering 85 new real-world software flaws within the OSS-Sydr-Fuzz project. Finally, we open Casr source code to the community to facilitate examination of the existing crashes.

关键词： Productivity Source coding Pipelines Computer bugs Fuzzing Benchmark testing Minimization

来源：评论

学校读者我要写书评

暂无评论

Implementation of Regularized Equations for the Disk Pump Simulation Problem in OpenFOAM

Implementation of Regularized Equations for the Disk Pump Si...

引用

Ivannikov ISPras Open Conference (ISPras)

作者： Tatiana Stenina Tatiana Elizarova Daniil Ryazanov Eugene Ryabinkin Ivannikov Institute for System Programming of the RAS Lomonosov Moscow State University Keldysh Institute of Applied Mathematics of the RAS Moscow Institute of Physics and Technology NRC Kurchatov Institute

Creating an effective pump that is able to maintain blood circulation in a heart with appropriate medical indications is undoubtedly a crucial task. First versions of such devices are currently being created and tested on the basis of IFPM SB ras, Novosibirsk. This work is devoted to a pump numerical simulations in order to optimize parameters. Equations of viscous incompressible fluid flow are used for this purpose. Implemented numerical algorithm is based on the regularization of the initial equations, which applies a finite volume method that avoids limiting procedures and includes them controlled numerical dissipation. Calculations are carried out within open software package OpenFOAM is installed at ISP ras. Unsteady flow in the pump is studied.

关键词： Mathematical model Computational modeling Blood Numerical models Geometry Trajectory Rotors

来源：评论

学校读者我要写书评

暂无评论

Symbolic Security Predicates: Hunt Program Weaknesses

Symbolic Security Predicates: Hunt Program Weaknesses

引用

Ivannikov ISPras Open Conference (ISPras)

作者： Alexey Vishnyakov Vlada Logunova Eli Kobrin Daniil Kuts Darya Parygina Andrey Fedotov Ivannikov Institute for System Programming of the RAS Moscow Institute of Physics and Technology Moscow Russia Lomonosov Moscow State University

ISBN: (纸本)9781665423311

Dynamic symbolic execution (DSE) is a powerful method for path exploration during hybrid fuzzing and automatic bug detection. We propose security predicates to effectively detect undefined behavior and memory access violation errors. Initially, we symbolically execute program on paths that don't trigger any errors (hybrid fuzzing may explore these paths). Then we construct a symbolic security predicate to verify some error condition. Thus, we may change the program data flow to entail null pointer dereference, division by zero, out-of-bounds access, or integer overflow weaknesses. Unlike static analysis, dynamic symbolic execution does not only report errors but also generates new input data to reproduce them. Furthermore, we introduce function semantics modeling for common C/C++ standard library functions. We aim to model the control flow inside a function with a single symbolic formula. This assists bug detection, speeds up path exploration, and overcomes overconstraints in path predicate. We implement the proposed techniques in our dynamic symbolic execution tool Sydr. Thus, we utilize powerful methods from Sydr such as path predicate slicing that eliminates irrelevant constraints. We present Juliet Dynamic to measure dynamic bug detection tools accuracy. The testing system also verifies that generated inputs trigger sanitizers. We evaluate Sydr accuracy for 11 CWEs from Juliet test suite. Sydr shows 95.59% overall accuracy. We make Sydr evaluation artifacts publicly available to facilitate results reproducibility.

关键词： Computer bugs Semantics Static analysis Fuzzing Libraries Reproducibility of results Security

来源：评论

学校读者我要写书评

暂无评论

Micro-Workflows Data Stream Processing Model for Industrial Internet of Things

Supercomputing Frontiers and Innovations

引用

Supercomputing Frontiers and Innovations 2021年第1期8卷 82-98页

作者： Alaasam, Ameer B.A. Radchenko, Gleb I. Tchernykh, Andrei N. South Ural State University Chelyabinsk Russia CICESE Research Center Ensenada Mexico Ivannikov Institute for System Programming of the RAS Russia

The fog computing paradigm has become prominent in stream processing for IoT systems where cloud computing struggles from high latency challenges. It enables the deployment of computational resources between the edge and cloud layers and helps to resolve constraints, primarily due to the need to react in real-time to state changes, improve the locality of data storage, and overcome external communication channels’ limitations. There is an urgent need for tools and platforms to model, implement, manage, and monitor complex fog computing workflows. Traditional scientific workflow management systems (SWMSs) provide modularity and flexibility to design, execute, and monitor complex computational workflows used in smart industry applications. However, they are mainly focused on batch execution of jobs consisting of tightly coupled tasks. Integrating data streams into SWMSs of IoT systems is challenging. We proposed a microworkflow model to redesign the monolith architecture of workflow systems into a set of smaller and independent workflows that support stream processing. Micro-workflow is an independent data stream processing service that can be deployed on different layers of the fog computing environment. To validate the feasibility and practicability of the micro-workflow refactoring, we provide intensive experimental analysis evaluating the interval between sensor messages, the time interval required to create a message, between sending sensor message and receiving the message in SWMS, including data serialization, network latency, etc. We show that the proposed decoupling support of the independence of implementation, execution, development, maintenance, and cross-platform deployment, where each micro-workflow becomes a standalone computational unit, is a suitable mechanism for IoT stream processing. © The Authors 2021. This paper is published with open access at ***.

关键词： Fog computing

来源：评论

学校读者我要写书评

暂无评论

Test Derivation against Timed Finite State Machines with Output Timed Guards

Test Derivation against Timed Finite State Machines with Out...

引用

International Russian Automation Conference (RusAutoCon)

作者： Aleksandr Tvardovskii Nina Yevtushenko National Research Tomsk State University Tomsk Russia Ivannikov Institute for System Programming of the RAS Moscow Russia

Approaches based on state machines are widely used to obtain guaranteed error coverage tests for discrete event systems. Many modern systems have time-dependent components, and thus, state machines are extended with clock variables and various time aspects, i.e. test synthesis methods must be adapted to new timed models. In this article, we consider Finite State Machines (FSM) with timeouts, input and output timed guards and show, how a test suite with guaranteed error coverage can be derived based on this model. The fault model and test derivation methods are based on the abstraction of the timed machine, i.e., on the FSM that describes the relevant aspects of the timed behavior. We consider two strategies for obtaining complete test suites under the assumption that the specification can be non-deterministic.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：