Edit automata: enforcement mechanisms for run-time security policies

We analyze the space of security policies that can be enforced by monitoring and modifying programs at run time. Our program monitors, called edit automata, are abstract machines that examine the sequence of application program actions and transform the sequence when it deviates from a specified policy. Edit automata have a rich set of transformational powers: they may terminate an application, thereby truncating the program action stream; they may suppress undesired or dangerous actions without necessarily terminating the program; and they may also insert additional actions into the event stream.After providing a formal definition of edit automata, we develop a rigorous framework for reasoning about them and their cousins: truncation automata (which can only terminate applications), suppression automata (which can terminate applications and suppress individual actions), and insertion automata (which can terminate and insert). We give a set-theoretic characterization of the policies each sort of automaton can enforce, and we provide examples of policies that can be enforced by one sort of automaton but not another.     

Enhancing web browser security against malware extensions

In this paper we examine security issues of functionality extension mechanisms supported by web browsers. Extensions (or “plug-ins”) in modern web browsers enjoy unrestrained access at all times and thus are attractive vectors for malware. To solidify the claim, we take on the role of malware writers looking to assume control of a user’s browser space. We have taken advantage of the lack of security mechanisms for browser extensions and implemented a malware application for the popular Firefox web browser, which we call browserSpy, that requires no special privileges to be installed. browserSpy takes complete control of the user’s browser space, can observe all activity performed through the browser and is undetectable. We then adopt the role of defenders to discuss defense strategies against such malware. Our primary contribution is a mechanism that uses code integrity checking techniques to control the extension installation and loading process. We describe two implementations of this mechanism: a drop-in solution that employs JavaScript and a faster, in-browser solution that makes uses of the browser’s native cryptography implementation. We also discuss techniques for runtime monitoring of extension behavior to provide a foundation for defending threats posed by installed extensions.     

Formal enforcement of security policies on concurrent systems

This paper introduces a formal and modular technique allowing to automatically enforce a security policy on a given concurrent system. Given a concurrent program P and a security policy ?, we automatically generate another program P^′ that satisfies ? and behaves like P, except that it stops when P tries to violate the security policy ?. We use extended version of process algebra ACP (Algebra of Communicating Process) and BPA (Basic Process Algebra) as formal languages to specify both concurrent system and security policy.     

Achieving dynamicity in security policies enforcement using aspects

The dynamic configuration and evolution of large-scale heterogeneous systems has made the enforcement of security requirements one of the most critical phases throughout the system development lifecycle. In this paper, we propose a framework architecture to associate the security policies with the specification and the execution phases of applications defined for these systems. Our proposed framework is based on an aspect-oriented programming approach and on the organization-based access control model to dynamically enforce and manage the access and the usage control. The deployment of the framework modules, proposed in this paper, takes into account the changes that may occur in the security policy during the application execution. We also present the implementation as well as the evaluation of our proposition.     

JavaScript引擎漏洞检测方法综述

由于语言特性导致的JavaScript引擎漏洞是当今应用软件软件安全的重要威胁之一,攻击者通常间接利用JavaScript引擎漏洞造成远程命令执行,获得系统的控制权。介绍了引擎的基本信息,对引擎中经常出现的漏洞进行了分类,分别综述了静态和动态分析检测的基本步骤和发展脉络,提出了针对JavaScript引擎漏洞的检测基本框架,讨论了制约检测效率瓶颈问题以及可能的解决方法,结合最新的技术应用指出了未来的发展趋势和亟待解决的问题。     

Android操作系统浏览器安全漏洞的分析

本文对Android操作系统中浏览器引擎WebKit工作原理进行分析,并介绍了WebView工作流程中存在安全漏洞,会造成用户个人信息丢失的隐患。根据Android操作系统中浏览器工作原理的分析,仿真验证了在WebView中确实存在用户人隐私信息丢失的危险。     

Kynoid: Real-time enforcement of fine-grained,user-defined,and data-centric security policies for Android

We introduce Kynoid, a real-time monitoring and enforcement framework for Android. Kynoid is based on user-defined security policies which are defined for data-items. This allows users to define temporal, spatial, and destination constraints which have to hold for single items. We introduce an innovative approach to allow for the real-time tracking and enforcement of such policies. In this way, Kynoid is the first extension for Android which enables the enforcement of security policies of data-items stored in shared resources. We outline Kynoid's architecture, present its operation and discuss it in terms of applicability, and performance. By providing a proof-of-concept implementation we further show the feasibility of our framework.     

基于Web浏览器的SSL VPN网关系统的设计和实现

在分析IPSec VPN与SSLVPN各自优劣势的基础上,提出了一种基于Web浏览器的SSL VPN网关系统的体系结构并给出了具体的实现方法.系统主要由HTTP协议代理Applet、VPN网关上的Web服务器和VPN反向代理服务器组成.系统提供了两种安全访问内网的模式,即隧道模式和替换模式.用户直接通过浏览器从VPN网关上下载Applet或点击用户界面中提供的资源列表就可以安全地访问内部网络中的资源.     

Verification and enforcement of access control policies

Access control mechanisms protect critical resources of systems from unauthorized access. In a policy-based management approach, administrators define user privileges as rules that determine the conditions and the extent of users’ access rights. As rules become more complex, analytical skills are required to identify conflicts and interactions within the rules that comprise a system policy—especially when rules are stateful and depend on event histories. Without adequate tool support such an analysis is error-prone and expensive. In consequence, many policy specifications are inconsistent or conflicting that render the system insecure. The security of the system, however, does not only depend on the correct specification of the security policy, but in a large part also on the correct interpretation of those rules by the system’s enforcement mechanism. In this paper, we show how policy rules can be formalized in Fusion Logic, a temporal logic for the specification of behavior of systems. A symbolic decision procedure for Fusion Logic based on Binary Decision Diagrams (BDDs) is provided and we introduce a novel technique for the construction of enforcement mechanisms of access control policy rules that uses a BDD encoded enforcement automaton based on input traces which reflect state changes in the system. We provide examples of verification of policy rules, such as absence of conflicts, and dynamic separation of duty and of the enforcement of policies using our prototype implementation (FLCheck) for which we detail the underlying theory.     

浏览器WEB安全威胁检测技术研究与实现

WEB浏览器是一种常见的客户端应用程序,是用户与网络交互的最主要平台之一,WEB应用已经广泛应用到新闻资讯、电子商务、社交网络等多个领域,然而由于WEB应用程序功能性和交互性的不断增强,对应的WEB漏洞和恶意攻击层出不穷,现有的WEB安全措施主要集中于服务端,然而客户端的安全机制相对比较薄弱,因此,对于如何保证WEB应用的安全己成为安全界广泛关注的重点。本文主要研究浏览器端的WEB安全威胁检测技术与实现。     

Formal enforcement and management of obligation policies

Obligations are generally actions that users are required to take and are essential for the expression of a large number of requirements. For instance, obligation actions may represent prerequisites to gain some privilege (pre obligations), to satisfy some ongoing or post requirement for resource usage (ongoing and post obligations), or to adhere to some privacy or availability policy. Obligations may also define states of affairs which should be maintained. An example of such obligations is the obligation “doctors should remain alert while in the operating room”. In this paper, we introduce a formal framework for the management and enforcement of obligation policies. The framework is formalized using concepts from action specification languages and the Event Condition Action paradigm of active databases. Therefore, our framework allows reasoning about change in the state of obligations and, at the same time, provides declarative formal semantics for their enforcement. In this framework, we support many types of obligations and show how to manage obligation activation, fulfillment and violation.     

ABAC策略语义表示和决策方法

为解决开放式系统环境中基于属性的访问控制（Attribute—Based Access Control,ABAC）策略语义层次上的表示和决策问题,提出了ABAC策略的本体表示方法。该方法基于ABAC策略模型到描述逻辑定义的映射,使用语义Web规则语言（swRL）处理系统内部关系定义。在此基础上,提出了基于封闭世界和实例实现推理的策略决策框架。最后从可靠性和完备性两方面说明了决策方法的正确性,验证实验表明了方法在实际应用中的适用性。     

基于Java2安全体系结构的Web数据库安全性问题研究

在Web应用系统中,Web数据库保护是关键,通过分析Java2安全平台中的安全体系结构核心、加密体系结构和Java2安全平台扩展中的验证授权服务、安全套接扩展、加密扩展,针对Web应用系统的三层结构模型,提出了基于Java2安全体系结构中的用户验证、保护数据库连接、访问控制和审计4大机制的Web数据库安全保护措施及具体的实现方法,为用户开发Web应用系统提供参考.     

Consistent policy enforcement in distributed systems using mobile policies

This paper briefly traces the evolution of information system architectures from mainframe-connected terminals to distributed multi-tier architectures. It presents the challenges facing developers of multi-tier information systems in providing effective consistent data policy enforcement, such as access control in these architectures. Finally, it introduces “Mobile Policy” (MoP) as a potential solution and presents a framework for using mobile policy in the business logic tier of multi-tier information systems.     

Validating a web service security abstraction by typing

An XML web service is, to a first approximation, an RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. We consider the problem of authenticating requests and responses at the SOAP-level, rather than relying on transport-level security. We propose a security abstraction, inspired by earlier work on secure RPC, in which the methods exported by a web service are annotated with one of three security levels: none, authenticated, or both authenticated and encrypted. We model our abstraction as an object calculus with primitives for defining and calling web services. We describe the semantics of our object calculus by translating to a lower level language with primitives for message passing and cryptography. To validate our semantics, we embed correspondence assertions that specify the correct authentication of requests and responses. By appeal to the type theory for cryptographic protocols of Gordon and Jeffrey's Cryptyc, we verify the correspondence assertions simply by typing. Finally, we describe an implementation of our semantics via custom SOAP headers. Received December 2003 Revised November 2004 Accepted December 2004 by A. E. Abdallah, P. Y. A. Ryan, S. A. Schneider and D. J. Cooke     

Security policies enforcement using finite and pushdown edit automata

Edit automata have been introduced by J.Ligatti et al. as a model for security enforcement mechanisms which work at run time. In a distributed interacting system, they play a role of a monitor that runs in parallel with a target program and transforms its execution sequence into a sequence that obeys the security property. In this paper, we characterize security properties which are enforceable by finite edit automata (i.e. edit automata with a finite set of states) and deterministic context-free edit automata (i.e. finite edit automata extended with a stack). We prove that the properties enforceable by finite edit automata are a sub-class of regular sets. Moreover, given a regular set $P$ , one can decide in time $O(n^2)$ , whether $P$ is enforceable by a finite edit automaton (where $n$ is the number of states of the finite automaton recognizing $P$ ) and we give an algorithm to synthesize the controller. Moreover, we prove that safety policies are always enforced by a deterministic context-free edit automaton. We also prove that it is possible to check if a policy is a safety policy in $O(n^4)$ . Finally, we give a topological condition on the deterministic automaton expressing a regular policy enforceable by a deterministic context-free edit automaton.     

动态安全策略的权限撤销研究

在分析以往安全操作系统中权限撤销机制的基础上,提出一种基于VTC和in progress 交叉链表的权限撤销机制。该机制通过对权限有效性、时效性检查以及in progress权限双向搜索实现权限撤销,并在基于L4微内核的原型系统中得以实现。实验表明,该撤销机制增加了1%左右的系统性能损耗。     

Web服务消息级安全模型的设计及评价

保证Web服务安全通信的机制有两种：传输级安全机制紧密耦合于下层平台,只能保证点到点的安全通信;而消息级安全机制能够提供异质环境的端到端安全保证.在WS-Security、SAML和XKMS等有关消息级安全的规范基础上,设计了一消息安全模型,并对其进行了安全性评价.该模型能够保证SOAP消息的机密性、完整性、不可否认性、认证和授权,能够保证Web服务的安全.