arXiv 1007.31832010-07-19cs.PL

A Non-Null Annotation Inferencer for Java Bytecode

Laurent Hubert

发表信息：: PASTE: Program analysis for software tools and engineering, Atlanta, Georgia : United States (2008)
DOI：: 10.1145/1512475.1512484

英文摘要：

We present a non-null annotations inferencer for the Java bytecode language. We previously proposed an analysis to infer non-null annotations and proved it soundness and completeness with respect to a state of the art type system. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Formal Certification of Android Bytecode

Android is an operating system that has been used in a majority of mobile devices. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are developed using Java, compiled to Java bytecode and then translated to DEX bytecode using the dx tool in the Android SDK. In this work, we aim to develop a type-based method for certifying non-interference properties of DEX bytecode, following a methodology that has been developed for Java bytecode certification by Barthe et al. To this end, we develop a…

2016-10-06cs.PL

Deadlock detection of Java Bytecode

This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language -- the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.

2017-09-13cs.PL

Non-Termination Analysis of Java Bytecode

We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The technique consists in compiling P into a constraint logic program P_CLP and in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implement…

2014-01-21cs.PL

Verification of Java Bytecode using Analysis and Transformation of Logic Programs

State of the art analyzers in the Logic Programming (LP) paradigm are nowadays mature and sophisticated. They allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. The aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (JVML). In order to achieve our goal, we rely on well-known techniques for meta-programming and program specialization. More precisely, we propose to partially evaluate a JVML interpreter implemented in LP together with (an LP representat…

2010-07-19cs.PL

A Framework for Debugging Java Programs in a Bytecode

In the domain of Software Engineering, program analysis and understanding has been considered to be a very challenging task since decade, as it demands dedicated time and efforts. The analysis of source code may occasionally be comparatively easier due to its static nature, however, the back end code (Bytecode), especially in terms of Java programming, is complicated to be analysed. In this paper, we present a methodological approach towards understanding the Bytecode of Java programs. We put forward a framework for the debugging process of Java Bytecode. Furthermore, we discuss the debugging …

2019-04-29cs.FLcs.PLcs.SE

Efficient and Expressive Bytecode-Level Instrumentation for Java Programs

We present an efficient and expressive tool for the instrumentation of Java programs at the bytecode-level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a light-weight Java bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The language is inspired by the aspect-oriented programming paradigm in modularizing instrumentation into separate transformers, that encapsulate joinpoint selection and advice inlining. BISM allows capturing joinpoints ranging from bytecode instructions to methods execution and provides comp…

2021-06-02cs.PLcs.SE

更多相关论文收起更多论文

JBMC: A Bounded Model Checking Tool for Java Bytecode

JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC relies on an operational model of the Java libraries, which conservatively approximates their semantics, to verify assertion violations, array out-of-bounds, unintended arithmetic overflows, and other kinds of functional and runtime errors in Java bytecode. JBMC can be used to either falsify properties or prove program correctness if an upper bound on the depth of the state-space is known. Practical applications of JBMC include but are not limited to bug finding, property checking, test inpu…

2023-02-05cs.LOcs.PLcs.SE

Towards a General Framework for Formal Reasoning about Java Bytecode Transformation

Program transformation has gained a wide interest since it is used for several purposes: altering semantics of a program, adding features to a program or performing optimizations. In this paper we focus on program transformations at the bytecode level. Because these transformations may introduce errors, our goal is to provide a formal way to verify the update and establish its correctness. The formal framework presented includes a definition of a formal semantics of updates which is the base of a static verification and a scheme based on Hoare triples and weakest precondition calculus to reaso…

2013-07-31cs.LOcs.PL

在 Java 字节码层面验证功能正确性属性

Verifying Functional Correctness Properties At the Level of Java Bytecode

本文提出在 Java 字节码层面工作的验证技术 ByteBack，通过源码级规约库与类型、表达式信息重建，验证多版本 Java 及现代特性编译出的字节码。

2024-09-30cs.LOcs.PL

在 Java 字节码层面推理异常行为

Reasoning About Exceptional Behavior At the Level of Java Bytecode

本文扩展 ByteBack，提出通过 Vimp 中间层在 Java 字节码层面建模并验证异常行为，可支持多版本 Java 及 Scala、Kotlin。

2024-09-30cs.LOcs.PL

SNITCH: Dynamic Dependent Information Flow Analysis for Independent Java Bytecode

Software testing is the most commonly used technique in the industry to certify the correctness of software systems. This includes security properties like access control and data confidentiality. However, information flow control and the detection of information leaks using tests is a demanding task without the use of specialized monitoring and assessment tools. In this paper, we tackle the challenge of dynamically tracking information flow in third-party Java-based applications using dependent information flow control. Dependent security labels increase the expressiveness of traditional info…

2019-08-27cs.PLcs.SE

Java 源代码仓库中提交变更的编译

Compilation of Commit Changes within Java Source Code Repositories

本文提出 JESS 方法，通过仅编译提交中修改的相关代码并自动推断存根，解决了 Java 项目中修复提交难以编译为字节码的问题，显著提升了漏洞补丁字节码的获取效率。

2024-07-25cs.PLcs.SE

Improving the Performance of the Paisley Pattern-Matching EDSL by Staged Combinatorial Compilation

Paisley is a declarative lightweight embedded domain-specific language for expressive, non-deterministic, non-invasive pattern matching on arbitrary data structures in Java applications. As such, it comes as a pure Java library of pattern-matching combinators and corresponding programming idioms. While the combinators support a basic form of self-optimization based on heuristic metadata, overall performance is limited by the distributed and compositional implementation that impedes non-local code optimization. In this paper, we describe a technique for improving the performance of Paisley tran…

2019-08-29cs.PL

完善面向对象语言中的函数式方法

Completing the Functional Approach in Object-Oriented Languages

针对面向对象语言中函数式特性零散的问题，提出基于Java的Java-TX语言，通过全局类型推断、真实函数类型等特性完善函数式方法，重点实现类型参数自动推断与函数类型异构转换以保留字节码类型信息。

2024-12-04cs.PL

JooFlux: Hijacking Java 7 InvokeDynamic To Support Live Code Modifications

Changing functional and non-functional software implementation at runtime is useful and even sometimes critical both in development and production environments. JooFlux is a JVM agent that allows both the dynamic replacement of method implementations and the application of aspect advices. It works by doing bytecode transformation to take advantage of the new invokedynamic instruction added in Java SE 7 to help implementing dynamic languages for the JVM. JooFlux can be managed using a JMX agent so as to operate dynamic modifications at runtime, without resorting to a dedicated domain-specific l…

2012-10-03cs.OScs.PL