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

SafeDrop: Detecting Memory Deallocation Bugs of Rust Programs via Static data-flow analysis

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 2023年第4期32卷 82-82页

作者： Cui, Mohan Chen, Chengjun Xu, Hui Zhou, Yangfan Fudan Univ Sch Comp Sci Shanghai Peoples R China Shanghai Key Lab Intelligent Informat Proc Shanghai Peoples R China

Rust is an emerging programming language that aims to prevent memory-safety bugs. However, the current design of Rust also brings side effects, which may increase the risk of memory-safety issues. In particular, it employs ownership-based resource management and enforces automatic deallocation of unused resources without using the garbage collector. It may therefore falsely deallocate reclaimed memory and lead to use-after-free or double-free issues. In this article, we study the problem of invalid memory deallocation and propose SafeDrop, a static path-sensitive data-flow analysis approach to detect such bugs. Our approach analyzes each function of a Rust crate iteratively in a flow-sensitive and field-sensitive way. It leverages a modified Tarjan algorithm to achieve scalable path-sensitive analysis and a cache-based strategy for efficient inter-procedural analysis. We have implemented our approach and integrated it into the Rust compiler. Experiment results show that the approach can successfully detect all such bugs in our experiments with a limited number of false positives and incurs a very small overhead compared to the original compilation time.

关键词： Rust data-flow analysis meet over path path sensitivity

来源：评论

学校读者我要写书评

暂无评论

Discovering and understanding android sensor usage behaviors with data flow analysis

引用

WORLD WIDE WEB-INTERNET AND WEB INFORMATION SYSTEMS 2018年第1期21卷 105-126页

作者： Liu, Xing Liu, Jiqiang Wang, Wei He, Yongzhong Zhang, Xiangliang Beijing Jiaotong Univ Beijing Key Lab Secur & Privacy Intelligent Trans 3 Shangyuancun Beijing 100044 Peoples R China King Abdullah Univ Sci & Technol Div Comp Elect & Math Sci & Engn Thuwal Saudi Arabia

Today's Android-powered smartphones have various embedded sensors that measure the acceleration, orientation, light and other environmental conditions. Many functions in the third-party applications (apps) need to use these sensors. However, embedded sensors may lead to security issues, as the third-party apps can read data from these sensors without claiming any permissions. It has been proven that embedded sensors can be exploited by well designed malicious apps, resulting in leaking users' privacy. In this work, we are motivated to provide an overview of sensor usage patterns in current apps by investigating what, why and how embedded sensors are used in the apps collected from both a Chinese app. market called "AppChina" and the official market called "Google Play". To fulfill this goal, We develop a tool called "SDFDroid" to identify the used sensors' types and to generate the sensor data propagation graphs in each app. We then cluster the apps to find out their sensor usage patterns based on their sensor data propagation graphs. We apply our method on 22,010 apps collected from AppChina and 7,601 apps from Google Play. Extensive experiments are conducted and the experimental results show that most apps implement their sensor related functions by using the third-party libraries. We further study the sensor usage behaviors in the third-party libraries. Our results show that the accelerometer is the most frequently used sensor. Though many third-party libraries use no more than four types of sensors, there are still some third-party libraries registering all the types of sensors recklessly. These results call for more attentions on better regulating the sensor usage in Android apps.

关键词： Android system Sensor usage data-flow analysis Clustering

来源：评论

学校读者我要写书评

暂无评论

A New Framework for Global Object-oriented data-flow analysis

A New Framework for Global Object-oriented Data-flow Analysi...

引用

IEEE BEIJING SECTION(跨国电气电子工程师学会北京分会)

作者： XU Xiong,XU Guo-ai,ZHANG Miao Key Laboratory of network and information attack & defence technology of MOE Beijing University of Posts and Telecommunications Beijing 100876,China ZHUO Xin-jian School of Science Beijing University of Posts and Telecommunications Beijing 100876,China

conventional data-flow analysis technology has many disadvantages when applied to OOPL for the polymorphism,generic,and other special *** paper analyzes these disadvantages,and based on which,a new dataflow analysis framework for OOPL is *** develops a unified abstract syntax tree(UAST) of all object-oriented programming *** algorithms of global data-flow analysis for OOPL are *** special OOPL features are *** experiment proves that,using this framework and its algorithm set,we can identify security vulnerabilities and their attack paths accurately and efficiently.

关键词： static analysis OOPL data-flow analysis software security

来源：评论

学校读者我要写书评

暂无评论

Exploring Sensor Usage Behaviors of Android Applications Based on data flow analysis 34

Exploring Sensor Usage Behaviors of Android Applications Bas...

引用

34th IEEE International Performance, Computing, and Communications Conference (lPCCC)

作者： Liu, Xing Liu, Jiqiang Wang, Wei Beijing Jiaotong Univ Sch Comp & Informat Technol Beijing 100044 Peoples R China

ISBN: (纸本)9781467385909

Today's Android-powered smartphones are equipped with various embedded sensors, such as the motion sensors, the environmental sensors and the position sensors. Many functions in the third-party applications (apps) need to use these sensors. However, embedded sensors may lead to security issues, as the third-party apps can access data from these sensors without claiming any permissions. It has been proven that embedded sensors can be exploited by well designed malicious apps, resulting in leaking users' privacy. In this work, we are motivated to provide an up-to-date overview of sensor usage patterns in current apps by investigating what, why and how embedded sensors are used in all the apps collected from a complete app market. To fulfill this goal, We develop a tool called "SDFDroid" to identify the sensors' types and to generate the sensor data propagation paths in each app. We then cluster the apps to find out their sensor usage patterns based on their sensor data propagation paths. We apply our method on AppChina, a widely used Chinese Android app market. Extensive experiments are conducted and the experimental results show that most apps implement their sensor related functions by using the third-party libraries. We further study the sensor usage in the third-party libraries. Our results show the accelerometer sensor is the most frequently used sensor. Though many third-party libraries use no more than four types of sensors, there are some third-party libraries register all the types of sensors recklessly. These results show the need for better regulating the sensor usage in Android apps.

关键词： Android system Sensor usage data-flow analysis Clustering

来源：评论

学校读者我要写书评

暂无评论

data-flow frameworks for worst-case execution time analysis

引用

REAL-TIME SYSTEMS 2002年第3期22卷 183-227页

作者： Blieberger, J Vienna Univ Technol Dept Comp Aided Automat A-1040 Vienna Austria

The purpose of this paper is to introduce frameworks based on data-flow equations which estimate the worst-case execution time (WCET) of real-time programs. These frameworks allow several different WCET analysis techniques with various precisions, which range from naive approaches to exact analysis, provided exact knowledge on the program behavior is available. In addition, data-flow frameworks can also be used for symbolic analysis based on information derived automatically from the source code of the program.

关键词： real-time systems worst-case execution time data-flow analysis symbolic evaluation

来源：评论

学校读者我要写书评

暂无评论

CRYPTODY: Cryptographic Misuse analysis of IoT Firmware via data-flow Reasoning 24

CRYPTODY: Cryptographic Misuse Analysis of IoT Firmware via ...

引用

27th International Symposium on Research in Attacks, Intrusions and Defenses (RAID)

作者： Wang, Jianing Guo, Shanqing Diao, Wenrui Liu, Yue Duan, Haixin Liu, Yichen Liang, Zhenkai Natl Univ Singapore Singapore Singapore Shandong Univ Jinan Peoples R China Southeast Univ Nanjing Peoples R China QI ANXIN Grp Beijing Peoples R China Tsinghua Univ Beijing Peoples R China Zhongguancun Lab Beijing Peoples R China Quancheng Lab Jinan Peoples R China Indiana Univ Bloomington Bloomington IN USA

ISBN: (纸本)9798400709593

Cryptographic techniques form the foundation of the security and privacy of computing solutions. However, if cryptographic APIs are not invoked correctly, they can result in significant security problems. In this paper, we abstract the intricate crypto misuse detection problem as a data-flow reasoning task. Towards this end, we propose CrypTody, a novel logic-inference-based framework for detecting crypto misuses via reasoning about data flows on multi-architecture IoT firmware images. It carries out cross-architecture analysis, with detection strategies to reduce false positives and false negatives, such as cross-flow misuse inference. To evaluate the effectiveness of CrypTody, we conducted a large-scale experiment on 1,431 firmware images from 16 vendors. Our evaluation shows that 46% of the firmware images have high-risk misuses and 95% have at least one cryptographic misuse. In total, we find 6,624 potential crypto misuses, with 760 being cross-flow misuses that are not detected by existing solutions. We have responsibly disclosed portions of our findings to the relevant vendors. From the feedback, we note that CrypTody has a low false-positive rate for the confirmed misuses. Some typical cases have been assigned CVEs and fixed by the vendors.

关键词： Cryptographic misuse IoT firmware data-flow analysis

来源：评论

学校读者我要写书评

暂无评论

An Incremental Algorithm for Algebraic Program analysis

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2025年第POPL期9卷 1934-1961页

作者： Zhou, Chenyu Fang, Yuzhou Wang, Jingbo Wang, Chao Univ Southern Calif Los Angeles CA 90007 USA Purdue Univ W Lafayette IN USA

We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that consists of two distinct steps: computing a path expression that succinctly summarizes the set of program paths of interest, and interpreting the path expression using a properly-defined semantic algebra to obtain program properties of interest. In this context, the goal of an incremental algorithm is to reduce the analysis time by leveraging the intermediate results computed before the program changes. We have made two main contributions. First, we propose a data structure for efficiently representing path expression as a tree together with a tree-based interpreting method. Second, we propose techniques for efficiently updating the program properties in response to changes of the path expression. We have implemented our method and evaluated it on thirteen Java applications from the DaCapo benchmark suite. The experimental results show that both our method for incrementally computing path expression and our method for incrementally interpreting path expression are effective in speeding up the analysis. Compared to the baseline APA and two state-of-the-art APA methods, the speedup of our method ranges from 160x to 4761x depending on the types of program analyses performed.

关键词： Algebraic Program analysis data-flow analysis Side-channel analysis Incremental Algorithm

来源：评论

学校读者我要写书评

暂无评论

Augmenting Interpolation-Based Model Checking with Auxiliary Invariants 30th

Augmenting Interpolation-Based Model Checking with Auxiliary...

引用

30th International Symposium on Model Checking Software

作者： Beyer, Dirk Chien, Po-Chun Lee, Nian-Ze Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9783031661488;9783031661495

Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPACHECKER and evaluated it against mature SMT-based methods in CPACHECKER as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.

关键词： Software model checking Program invariants Invariant injection Craig interpolation data-flow analysis SMT SAT

来源：评论

学校读者我要写书评

暂无评论

Equivalence analysis: a general technique to improve the efficiency of data-flow analyses in the presence of pointers 99

Equivalence analysis: a general technique to improve the eff...

引用

Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

作者： Donglin Liang Mary Jean Harrold The Ohio State University

ISBN: (纸本)9781581131376

Existing methods to handle pointer variables during data-flow analyses can make such analyses inefficient both in time and space because the data-flow analyses must store and propagate large sets of data facts that are introduced by dereferences of pointer variable. This paper presents equivalence analysis, a general technique to improve the efficiency of data-flow analyses in the presence of pointers. The technique identifies equivalence relations among the memory locations accessed by a procedure and ensures that two equivalent memory locations share the same set of data facts in a procedure and in the procedures that are called by that procedure. Thus, a data-flow analysis needs to compute the data-flow information only for a representative memory location in an equivalence class. The data-flow information for other memory locations in the equivalence class can be derived from that of the representative memory location. Our empirical studies indicate that equivalence analysis may effectively improve the efficiency of many data-flow analyses.

关键词： alias analysis data-flow analysis

来源：评论

学校读者我要写书评

暂无评论

Automatic Generation of Interprocedural data—flow Analyzers and Optimizers

引用

Journal of Computer Science & Technology 2002年第6期17卷 708-717页

作者：连瑞奇张兆庆乔如良 Institute of Computing Technology The Chinese Academy of Sciences Beijing 100080 P.R. China

Interprocedural analysis and optimization are very important for compilers toexploit parallelism of modern high-performance computer systems. But it is very complicated,easy to make mistakes and difficult to maintain and port. To solve the problem, we construct anautomatic generator of interprocedural analyzers and optimizers - IGEN. In IGEN, first a newmodel to describe the interprocedural data-flow problem is designed. It is fit for all traditionaldata-flow problems and can be used in context-sensitive algorithms. Then, the structure andthe working environment of IGEN are described in detail. Finally, the implementation of IGENand our experimental result are given.

关键词： data-flow analysis interprocedural analysis and optimization automaticgenerator

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：