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

Interprocedural Static Analysis for Finding Bugs in Go Programs

programming AND COMPUTER SOFTWARE 2021年第5期47卷 344-352页

作者： Bolotnikov, I., V Borodin, A. E. Russian Acad Sci Ivannikov Inst Syst Programming Ul Solzhenitsyna 25 Moscow 119333 Russia Moscow MV Lomonosov State Univ Moscow 119991 Russia

In recent years, the popularity of the Go programming language has been growing. However, currently, there are only lightweight static analyzers (linters) available for Go. We fill this gap by adapting the Svace static analyzer for Go programs. We implement an interprocedural and intermodular static analyzer that possesses both flow sensitivity and path sensitivity. To evaluate its performance, we use ten open source projects. The sixteen evaluated checkers emitted 6817 warnings with 76% true positive rate.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Cloud Data Storage and Private Information Retrieval Algorithms

引用

programming AND COMPUTER SOFTWARE 2024年第6期50卷 425-434页

作者： Varnovskiy, N. P. Martishin, S. A. Khrapchenko, M. V. Shokurov, A. V. Lomonosov Moscow State Univ Informat Secur Sect Informat Secur Inst Moscow 119192 Russia Russian Acad Sci Ivannikov Inst Syst Programming Moscow 109004 Russia

The authors consider the private information retrieval (PIR) problem, in particular, the problem of ensuring secure queries to a database. Previously, the authors considered this problem for a cloud database in the presence of an active adversary who does not interfere with the execution of the PIR protocol but can carry out an attack with known open queries. In the proposed algorithms, bit number i is represented as an l-ary number with d digits. An algorithm for database placement on the cloud and an algorithm for bit querying with the use of permutations in the digits of a bit number, where bit number i is defined in a base-l number system, are proposed. The permutations are regarded as secret encryption keys. The communication complexity and the probability of guessing the bit number in a single attack with a known open query for bit number i, as well as in an attack with an unlimited number of known open queries, are estimated.

关键词： Structured Query Language

来源：评论

学校读者我要写书评

暂无评论

Intraprocedural Analysis Based on Symbolic Execution for Bug Detection

引用

programming AND COMPUTER SOFTWARE 2021年第8期47卷 858-865页

作者： Borodin, A. E. Dudina, I. A. Russian Acad Sci Ivannikov Inst Syst Programming Ul Solzhenitsyna 25 Moscow 109004 Russia Moscow MV Lomonosov State Univ Moscow 119991 Russia

In this paper, we overview the approaches and techniques employed by the Svace static analysis tool for intraprocedural analysis. This analysis implies the traversal of the control flow graph, symbolic execution with state merging, analysis of a number of paths in functions with loops, simultaneous run of all analyzers, modeling of accessible memory cells, and value numbering.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

On Effective Scheduling in Computing Clusters

引用

programming AND COMPUTER SOFTWARE 2019年第7期45卷 398-404页

作者： Grushin, D. A. Kuzyurin, N. N. Russian Acad Sci Ivannikov Inst Syst Programming Ul Solzhenitsyna 25 Moscow 109004 Russia Moscow Inst Phys & Technol Inst Skii 9 Dolgoprudnyi 141700 Moscow Oblast Russia

Presently, big companies such as Amazon, Google, Facebook, Microsoft, and Yahoo! own huge datacenters with thousands of nodes. These clusters are used simultaneously by many clients. The users submit jobs containing one or more tasks. The task flow is usually a mix of short, long, interactive, and batch tasks with different priorities. The cluster scheduler decides on which server the task should be run as a process, container, or virtual machine. Scheduler optimizations are important as they provide higher server utilization, lower latency, improved load balancing, and fault tolerance. Optimal task placement is a complex problem that has multiple dimensions and requires algorithmically complex optimizations. This increases placement latency and limits cluster scalability. In this paper, we consider different cluster scheduler architectures and optimization problems.

关键词： Fault tolerance

来源：评论

学校读者我要写书评

暂无评论

Dynamic Analysis of ARINC 653 RTOS with LLVM

Dynamic Analysis of ARINC 653 RTOS with LLVM

引用

ivannikov Ispras Open Conference (ISPRAS)

作者： Cheptsov, Vitaly Khoroshilov, Alexey Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia Higher Sch Econ Moscow Russia

ISBN: (纸本)9781728112756

Existing standards for airborne-embedded software systems impose a number of requirements applicable to the software development cycle of hard real-time operating systems found in modern aircraft. The measures taken are meant to reduce the risks of undesired consequences, but have strongly varying costs. Dynamic instrumentation and static analysis are common practices used to automatically find software defects, from strictly non-conforming code constructions to memory corruptions or invalid control flow. LLVM analyser and sanitizer infrastructure, while regularly applied to general-purpose software, originally was not thought to be introduced to heavily restricted environments. In this paper we discuss the specifics of airborne systems with regards to dynamic instrumentation and provide practical considerations to be taken into account for the effective use of general-purpose instrumentation tools. We bring a complete LLVM stack support to JetOS, a prospective onboard real-time operating system currently being developed at ISP RAS in collaboration with GosNIIAS. As an example, we port AddressSanitizer, MemorySanitizer, and UndefmedBehaviorSanitizer and provide the details against the caveats on all relevant sides: a sanitizer, a compiler, and an operating system. In addition we suggest uninvolved optimisations and enhancements to the runtimes to maximise the effects of the tools.

关键词： dynamic instrumentation real-time operating systems ARINC 653 IMA LLVM

来源：评论

学校读者我要写书评

暂无评论

Combining Static Analysis With Directed Symbolic Execution for Scalable and Accurate Memory Leak Detection

引用

IEEE ACCESS 2024年 12卷 80128-80137页

作者： Aslanyan, Hayk Movsisyan, Hovhannes Hovhannisyan, Hripsime Gevorgyan, Zhora Mkoyan, Ruslan Avetisyan, Arutyun Sargsyan, Sevak Russian Armenian Univ Ctr Adv Software Technol Yerevan 0051 Armenia Russian Acad Sci RAS Ivannikov Inst Syst Programming Moscow 109004 Russia

This article introduces a novel method for the precise and scalable detection of memory leaks comprising two primary stages. Initially, context-, flow-, and field-sensitive static analysis is used to identify potential memory leaks. This includes an annotation system that allows specifying key properties of functions. Therefore, they do not need to be reanalyzed every time they are called. It also allows manual annotation of important library or system functions, thus enhancing analysis quality. The static analysis is conducted in reverse topological order on the call graph, enabling the parallel processing of functions within the same level of hierarchy. Subsequently, directed symbolic execution provides path-sensitivity and effectively filters out false positives. This process is performed concurrently for each bug detected by static analysis. This two-stage approach aims to enhance the efficiency and precision of memory leak detection in industrial software. The proposed method was implemented in the MLH (Memory Leak Hunter) tool, which identified numerous bugs in the open-source software, including OpenSSL, FFmpeg, and Radare2. These bugs were reported and confirmed by the community, thereby proving the effectiveness of the developed method.

关键词： Directed symbolic execution static analysis memory leak

来源：评论

学校读者我要写书评

暂无评论

Toward to usage of regularized Stefan problem solution in icing modeling

Toward to usage of regularized Stefan problem solution in ic...

引用

ivannikov Ispras Open Conference (ISPRAS)

作者： Ivanov, Alexander, V Levin, Mikhail P. Stenina, Tatiana, V Strijhak, Sergey, V Russian Acad Sci Ivannikov Inst Syst Programming 25 Alexander Solzhenitsyn St Moscow 109004 Russia

ISBN: (纸本)9781665412919

In 2019 Tong Liu and coauthors proposed the development of the Messinger-Myers models for modeling the icing of aircraft. Their proposal consists in replacing the quasi-stationary heat equation for the ice region with a non-stationary heat equation. In our work, we propose to consider the same replacement for the water film region also. Then in the region of ice and water film, the temperature is described by a unified equation of thermal conductivity with discontinuous coefficients at the interface is known as Stefan problem. Stefan problem is a fundamental problem describing phenomena in phase transitions of substance. It was investigated as analytically and numerical both by various authors. Due to complexity of the considering problem the analytics is available only in simple cases. The main complexity of this problem relates with the internal boundary moving. The numerical solution of this incorrect problem is not simple. To date, a few of regularization methods proposed for the solution of Stefan problems by various authors. The main goal of this paper is investigate regularization of considering problem by omitting of classic Stefan condition at interface boundary. For solving of regularized problem we apply two different finite difference schemes of the second order approximation. The first is a second order hybrid finite difference scheme in and the second is a uniform second order finite difference scheme. Computations in Open Source Octave environment were provided and numerical results obtained by different schemes compared together, and with analytical solution. Computations of ice accretion on the NACA 0012 airfoil computed by iceFoam solver and Messenger-Mayer model are presented.

关键词： Stefan problem moving boundary problems phase transition problems discontinuous coefficient problem finite differences schemes hybrid schemes iceFoam solver

来源：评论

学校读者我要写书评

暂无评论

Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic

引用

programming AND COMPUTER SOFTWARE 2022年第8期48卷 770-780页

作者： Sadykov, R. F. Mandrykin, M. U. Moscow MV Lomonosov State Univ Moscow 119991 Russia Russian Acad Sci Ivannikov Inst Syst Programming ul Solzhenitsyna 25 Moscow 109004 Russia

The process of developing C programs is quite often prone to errors associated with the use of pointer arithmetic and operations on memory addresses. Hence, the need for various automated program verification tools arises. One of the techniques frequently employed by these tools is invocation of suitable decision procedures implemented within existing SMT solvers. However, both the SMT standard and the majority of existing SMT solvers lack relevant logics (combinations of logical theories) for the direct and precise modeling of the semantics of pointer operations in C. A possible way to support these logics is to implement them in an SMT solver. However, this approach can be time-consuming (as it requires modifying the source code of the solver), inflexible (because introducing any changes to the signature or semantics of the theory can be unreasonably hard), and limited (every solver has to be supported individually). Another way is to design and implement custom quantifier instantiation strategies. These strategies can then be used to translate formulas in selected theory combinations into formulas in well-supported decidable logics, e.g., QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally prove the soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper also presents an informal description of this proof for the proposed procedure. The theory of bounded pointer arithmetic itself is formulated based on known errors associated with the use of pointer arithmetic operations in C, as well as based on the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to derive efficient decision procedures, implemented as

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Implementation of an iterative algorithm for the coupled heat transfer in case of high-speed flow around a body

引用

COMPUTERS & FLUIDS 2018年 172卷 483-491页

作者： Galanin, M. P. Zhukov, V. T. Klyushnev, N., V Kuzmina, K. S. Lukin, V. V. Marchevsky, I. K. Rodin, A. S. Russian Acad Sci Keldysh Inst Appl Math Moscow Russia Bauman Moscow State Tech Univ Moscow Russia Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia

The results of investigation of a numerical technique for coupled heat transfer problem solving for an atmospheric supersonic flying vehicle and flow around it are presented. An iterative numerical algorithm and software package are developed for heat transfer simulation in a flying vehicle structure during its motion in the atmosphere. The convergence of variants of the iterative process for solution matching on the surface with ideal thermal contact is studied. The results of the numerical experiment confirm the obtained theoretical estimates. (C) 2018 Elsevier Ltd. All rights reserved.

关键词： Heat transfer Coupled problem Numerical experiment Supersonic flow Shock wave

来源：评论

学校读者我要写书评

暂无评论

Data Reliability and Redundancy Optimization of a Secure Multi-Cloud Storage Under Uncertainty of Errors and Falsifications 33

Data Reliability and Redundancy Optimization of a Secure Mul...

引用

33rd IEEE International Parallel and Distributed Processing Symposium (IPDPS)

作者： Tchernykh, Andrei Babenko, Mikhail Kuchukov, Viktor Miranda-Lopez, Vanessa Avetisyan, Arutyun Rivera-Rodriguez, Raul Radchenko, Gleb CICESE Res Ctr Ensenada Baja California Mexico South Ural State Univ Chelyabinsk Russia Ivannikov Inst Syst Programming Moscow Russia North Caucasus Fed Univ Stavropol Russia RAS Ivannikov Inst Syst Programming Moscow Russia

ISBN: (纸本)9781538655559

Despite all the benefits a cloud data storages offer to customers, there is a high risk of breach of confidentiality, integrity, and availability related with the uncertainty of errors and falsifications, loss of information, denial of access for a long time, information leakage, conspiracy, and technical failures. In this article, we propose a configurable, reliable, and secure distributed data storage scheme with improved data redundancy, reliability, and encoding/decoding speed. Our system utilizes a Polynomial Residue Number system (PRNS) with a new method of error correction codes and secret sharing schemes. We introduce the concept of an approximate value of a rank (AR) of a polynomial. It reduces the computational complexity of the encoding/decoding and PRNS coefficients size. Based on the properties of the approximate value and PRNS, we introduce the AR-PRNS method for error detection, correction, and controlling computational results with capabilities of scalable parallel computing. We provide a theoretical basis to configure and optimize the redundancy of stored data and encoding/decoding speed to cope with different objective preferences, workloads, and storage properties. Theoretical analysis shows that, by appropriate selection of AR-PRNS parameters, the proposed scheme increases the safety, reliability, and reduces the overhead of data storage.

关键词： cloud storage reliability polynomial residue number system secret sharing scheme security uncertainty

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：