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

Software Watermarking: A semantics-based Approach

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2017年 331卷 71-85页

作者： Dalla Preda, Mila Pasqua, Michele Univ Verona Dept Comp Sci Str Grazie 15 I-37134 Verona Italy

Software watermarking is a defence technique used to prevent software piracy by embedding a signature, i.e., an identifier reliably representing the owner, in the code. When an illegal copy is made, the ownership can be claimed by extracting this identifier. The signature has to be hidden inside the program and it has to be difficult for an attacker to detect, tamper or remove it. In this paper we show how the ability of the attacker to identify the signature can be modelled in the framework of abstract interpretation as a completeness property. We view attackers as abstract interpreters that can precisely observe only the properties for which they are complete. In this setting, hiding a signature in the code corresponds to inserting it in terms of a semantic property that can be retrieved only by attackers that are complete for it. Indeed, any abstract interpreter that is not complete for the property specifying the signature cannot detect, tamper or remove it. The goal of this work is to introduce a formal framework for the modelling, at a semantic level, of software watermarking techniques and their quality features.

关键词： Software Watermarking Abstract Interpretation program semantics program transformation

来源：评论

学校读者我要写书评

暂无评论

A LINKED FOREST MANIPULATION SYSTEM semantics RULES FOR AN ATTRIBUTED TRANSLATION GRAMMAR FOR PL/O

引用

INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS 1988年第1期24卷 1-28页

作者： MCCLUSKEY, CPS The Pennsylvania State University Computer Science Department Fogelsville PA 18051 United States

In this paper a linked forest manipulation system (abbreviated as LFMS) semantics rules is defined for an attributed translation grammar (abbreviated as ATG) for PL/0 defined and discussed by McCluskey [9]. The LFMS reflects the translation achieved by the ATG, which is the generation of theP-codes, used in the original interpreter by Wirth [12].

关键词： program semantics linked forest manipulation system attributed translation grammar code generation PL/0 D D.3 D.3.1 F F.3 F.3.2

来源：评论

学校读者我要写书评

暂无评论

Graph semantic similarity-based automatic assessment for programming exercises

引用

SCIENTIFIC REPORTS 2024年第1期14卷 1-14页

作者： Xiang, Chengguan Wang, Ying Zhou, Qiyun Yu, Zhen Cent China Normal Univ Fac Artificial Intelligence Educ Wuhan 430079 Peoples R China Guizhou Educ Univ Sch Math & Big Data Guiyang 550018 Peoples R China

This paper proposes an algorithm for the automatic assessment of programming exercises. The algorithm assigns assessment scores based on the program dependency graph structure and the program semantic similarity, but does not actually need to run the student's program. By calculating the node similarity between the student's program and the teacher's reference programs in terms of structure and program semantics, a similarity matrix is generated and the optimal similarity node path of this matrix is identified. The proposed algorithm achieves improved computational efficiency, with a time complexity of O ( n 2 ) \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$O(n<^>2)$$\end{document} for a graph with n nodes. The experimental results show that the assessment algorithm proposed in this paper is more reliable and accurate than several comparison algorithms, and can be used for scoring programming exercises in C/C++, Java, Python, and other languages.

关键词： Automatic assessment program dependency graph program semantics Similarity programming exercises

来源：评论

学校读者我要写书评

暂无评论

AN ATTRIBUTED TRANSLATION GRAMMAR FOR PL/O

引用

INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS 1987年第3-4期21卷 205-227页

作者： MCCLUSKEY, CPS The Pennsylvania State University Computer Science Department Fogelsville PA 18051 United States

In this paper an attributed translation grammar (abbreviated as ATG) for the PL/0 is defined. The translation achieved by the ATG is the generation of theP-codes, used in the original interpreter by Wirth [7]. Due (o backtracking which may be followed by trimming of subtrees after code generation, it is never necessary to have the complete derivation tree. This is true even with recursion.

关键词： program semantics attributed translation grammar code generation parsing tree PL/0 D.3 programmmg languages D.31 Formal definitions and theory semantics F.3 Logics and meanings of programs F3.2 semantics of programming languages operational semantics

来源：评论

学校读者我要写书评

暂无评论

Invariant relations, invariant functions, and loop functions

引用

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING 2012年第3期8卷 195-212页

作者： Jilani, Lamia Labed Louhichi, Asma Mraihi, Olfa Mili, Ali Inst Sup Gest Bardo 2000 Tunisia Inst Sup Inform & Multimedia Ariana 2080 Tunisia NJIT CCS Newark NJ 07102 USA

The increasing criticality of software applications, the increasing size and complexity of such applications, and the increasing reliance of software engineering paradigms on third party software assets combine to place a high premium on the ability to analyze software products to an arbitrary level of thoroughness and precision. Yet despite several decades of research, the goal of analyzing the functional properties of software products to an arbitrary level of thoroughness and precision remains unfulfilled. In this paper, we discuss the use of a relation-theoretic approach inspired from Mills' logic to analyze while loops, and we support our approach by an operational prototype tool. The proposed method and tool have applications in program comprehension, reverse engineering, program verification, software maintenance, and programmer education.

关键词： program analysis program semantics program function While loop Refinement calculus Reverse modeling

来源：评论

学校读者我要写书评

暂无评论

Inductive Completeness of Logics of programs

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年第C期228卷 101-112页

作者： Leivant, Daniel Indiana Univ Bloomington IN 47405 USA

We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for decades. The denotational semantics of a regular program can be construed as a relation, easily definable by structural induction on programs. Invoking the framework of canonical theories for (iterated) inductive definitions, we consider the first-order theory for program semantic, i.e. with the generative clauses as construction (introduction) rules, and their dual templates as deconstruction (elimination) rules. We prove that Hoare's logic is inductively complete, in the sense that a partial-correctness assertion is Hoare provable iff it is provable in the inductive theory (with deconstruction for formulas in the base vocabulary). Thus first-order automated theorem-proving can be applied directly to program verification. Proceeding to program termination, we show that a total correctness assertion is valid iff it is provable in the inductive theory without any use of deconstruction. This is yet another take on the first-order nature of total correctness.

关键词： Inductive definitions program semantics inductive completeness Hoare logic

来源：评论

学校读者我要写书评

暂无评论

A Rewriting semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第4期176卷 47-60页

作者： Katelman, Michael Meseguer, Jose Univ Illinois Dept Comp Sci Urbana IL 61801 USA

We present a rewriting logic semantics in Maude of the ABEL hardware description language. Based on this semantics, and on Maude's underlying LTL model checker, we propose a scalable formal analysis framework and tool for hardware/software co-design. The analysis method is based on trace checking of finite system behaviors against LTL temporal logic formulas. The formal properties of the hardware, the embedded software, and the interactions between both can all be analyzed this way. We present two case studies illustrating our method and tool.

关键词： co-verification co-design rewriting logic program semantics hardware description languages Maude

来源：评论

学校读者我要写书评

暂无评论

Harnessing a Refinement Theory to Compute Loop Functions

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年 243卷 139-155页

作者： Mili, Ali Ben Ayed, Rahma Aharon, Shir Nadkarni, Chaitanya New Jersey Inst Technol Coll Comp Sci Newark NJ 07102 USA Univ Tunis El Manar SysCom Ecole Natl Ingn Tunis Tunis Tunisia

We consider a while loop on some space S and we are interested in deriving the function that this loop defines between its initial states and its final states (when it terminates). Such a capability is useful in a wide range of applications, including reverse engineering, software maintenance, program comprehension, and program verification. In the absence of a general theoretical solution to the problem of deriving the function of a loop, we explore engineering solutions. In this paper we use a relational refinement calculus to approach this complex problem in a systematic manner. Our approach has many drawbacks, some surmountable and some not (being inherent to the approach);nevertheless, it offers a way to automatically derive the function of loops or an approximation thereof, under some conditions.

关键词： Reverse engineering software maintenance program comprehension while loops program semantics program correctness refinement calculi software tools

来源：评论

学校读者我要写书评

暂无评论

Characterizing a property-driven obfuscation strategy

引用

JOURNAL OF COMPUTER SECURITY 2018年第1期26卷 31-69页

作者： Dalla Preda, Mila Mastroeni, Isabella Univ Verona Dipartimento Informat Verona Italy

In recent years, code obfuscation has attracted both researchers and software developers as a useful technique for protecting secret properties of proprietary programs. The idea of code obfuscation is to modify a program, while preserving its functionality, in order to make it more difficult to analyze. Thus, the aim of code obfuscation is to conceal certain properties to an attacker, while revealing its intended behavior. However, a general methodology for deriving an obfuscating transformation from the properties to conceal and reveal is still missing. In this work, we start to address this problem by studying the existence and the characterization of function transformers that minimally or maximally modify a program in order to reveal or conceal a certain property. Based on this general formal framework, we are able to provide a characterization of the maximal obfuscating strategy for transformations concealing a given property while revealing the desired observational behavior. To conclude, we discuss the applicability of the proposed characterization by showing how some common obfuscation techniques can be interpreted in this framework. Moreover, we show how this approach allows us to deeply understand what are the behavioral properties that these transformations conceal, and therefore protect, and which are the ones that they reveal, and therefore disclose.

关键词： program transformation abstract interpretation program semantics code obfuscation

来源：评论

学校读者我要写书评

暂无评论

semantics-based code obfuscation by abstract interpretation

引用

JOURNAL OF COMPUTER SECURITY 2009年第6期17卷 855-908页

作者： Dalla Preda, Mila Giacobazzi, Roberto Univ Verona Dipartimento Informat Str Grazie 15 I-37134 Verona Italy

In recent years code obfuscation has attracted research interest as a promising technique for protecting secret properties of programs. The basic idea of code obfuscation is to transform programs in order to hide their sensitive information while preserving their functionality. One of the major drawbacks of code obfuscation is the lack of a rigorous theoretical framework that makes it difficult to formally analyze and certify the effectiveness of obfuscating techniques. We face this problem by providing a formal framework for code obfuscation based on abstract interpretation and program semantics. In particular, we show that what is hidden and what is preserved by an obfuscating transformation can be expressed as abstract interpretations of program semantics. Being able to specify what is masked and what is preserved by an obfuscation allows us to understand its potency, namely the amount of obscurity that the transformation adds to programs. In the proposed framework, obfuscation and attackers are modeled as approximations of program semantics and the lattice of abstract interpretations provides a formal tool for comparing obfuscations with respect to their potency. In particular, we prove that our framework provides an adequate setting to measure not only the potency of an obfuscation but also its resilience, i.e., the difficulty of undoing the obfuscation. We consider code obfuscation by opaque predicate insertion and we show how the degree of abstraction needed to disclose different opaque predicates allows us to compare their potency and resilience.

关键词： Code obfuscation abstract interpretation program semantics static program analysis

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：