Compositional Security, 2014

	Compositional Security 2014

The Hard Problem of composability and scalability remains a focus of the four Science of Security Lablets. However, aside from them, there was relatively little research reported in 2014 in this area.

Rafnsson, W.; Sabelfeld, A., “Compositional Information-Flow Security for Interactive Systems,” Computer Security Foundations Symposium (CSF), 2014 IEEE 27th, vol., no., pp. 277, 292, 19-22 July 2014. doi:10.1109/CSF.2014.27
Abstract: To achieve end-to-end security in a system built from parts, it is important to ensure that the composition of secure components is itself secure. This work investigates the compositionality of two popular conditions of possibilistic noninterference. The first condition, progress-insensitive noninterference (PINI), is the security condition enforced by practical tools like JSFlow, Paragon, sequential LIO, Jif, Flow Caml, and SPARK Examiner. We show that this condition is not preserved under fair parallel composition: composing a PINI system fairly with another PINI system can yield an insecure system. We explore constraints that allow recovering compositionality for PINI. Further, we develop a theory of compositional reasoning. In contrast to PINI, we show what PSNI behaves well under composition, with and without fairness assumptions. Our work is performed within a general framework for nondeterministic interactive systems.
Keywords: interactive systems; security of data; Flow Caml; JSFlow; Jif; PINI system; Paragon; SPARK Examiner; compositional information-flow security; compositional reasoning; end-to-end security; nondeterministic interactive systems; parallel composition; possibilistic noninterference; progress-insensitive noninterference; sequential LIO; Cognition; Computational modeling; Interactive systems; Security; Semantics; Sensitivity; Synchronization (ID#: 15-6038)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6957117&isnumber=6957090

Cong Sun; Ning Xi; Jinku Li; Qingsong Yao; Jianfeng Ma, “Verifying Secure Interface Composition for Component-Based System Designs,” Software Engineering Conference (APSEC), 2014 21st Asia-Pacific , vol.1, no., pp. 359, 366, 1-4 Dec. 2014. doi:10.1109/APSEC.2014.60
Abstract: Information flow security has been considered as a critical requirement on software systems, especially when heterogeneous components from different parties cooperate to achieve end-to-end enforcement on data confidentiality. Enforcing the information flow security properties on complicated systems faces a great challenge because the properties cannot be preserved under composition and most of the current approaches are not scalable enough. To address this problem, there have been several recent efforts on the compositional information flow analyses developed for different abstraction levels. But these approaches have rarely been considered to incorporate with the process of system design. Integrating the security enforcement with the model-based development process can provide the designer with ability to verify information flow security in the early stage of system development. We propose a compositional information flow verification which is integrated with model-based system design in Sys ML by an automated model translation from semi-formal behavior and structure models to interface automata. Our compositional approach is general to support the complex security lattices and a variety of in distinguish ability relations. The evaluation results show the usability of our approach on practical system designs and the scalability of the compositional verification.
Keywords: automata theory; object-oriented programming; security of data; software architecture; SysML; abstraction levels; automated model translation; complex security lattices; component-based system designs; compositional information flow analyses; data confidentiality; heterogeneous components; information flow security; interface automata; model-based development process; model-based system design; secure interface composition verification; security enforcement; semiformal behavior; software systems; structure models; Artificial intelligence; Automata; Component architectures; Lattices; Modeling; Security; Unified modeling language; component-based design; information flow; interface automata; model translation; model-based development; noninterference; systems modeling language (ID#: 15-6039)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7091331&isnumber=7091273

Alzubaidi, W.Kh.; Longzheng Cai; Alyawer, S.A., “Enhance the Performance of ICMP Protocol by Reduction the IP over Ethernet Naming Architecture,” Computer and Information Sciences (ICCOINS), 2014 International Conference on, vol., no.,
pp. 1, 6, 3-5 June 2014. doi:10.1109/ICCOINS.2014.6868392
Abstract: This study addresses the Internet Control Message Protocol (ICMP) performance problems arising in Internet protocol (IP) over Ethernet networks. These problems arise because of the compatibility issue between two different compositional protocols: the IP and Ethernet protocol. The motivation behind addressing the compatibility problem is to improve the security and performance of networks by studying the link compatibility between the Ethernet and IP protocols. The findings of this study have given rise to proposals for modifications. A reduction in the current naming architecture design is advocated to improve the performance and security of IP over Ethernet networks. The use of the IP address, as one flat address for the naming architecture, is proposed instead of using both the IP and Media Access Control (MAC) addresses. The proposed architecture is evaluated through a simulated cancellation of the use of the Address Resolution Protocol (ARP) protocol.
Keywords: IP networks; computer network performance evaluation; computer network security; local area networks; transport protocols; ARP protocol; Ethernet naming architecture; Ethernet protocol; ICMP performance problems; ICMP protocol performance; IP address; IP over Ethernet networks; IP protocols; Internet control message protocol; address resolution protocol; compatibility problem; compositional protocols; flat address; link compatibility; naming architecture design; network performance; security; Computer architecture; Computers; Ethernet networks; IP networks; Protocols; Security; Unicast; Ethernet Networks; ICMP; IP; MAC; Naming Architecture; Performance (ID#: 15-6040)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6868392&isnumber=6868339

Modersheim, S.; Katsoris, G., “A Sound Abstraction of the Parsing Problem,” Computer Security Foundations Symposium (CSF), 2014 IEEE 27th, vol., no., pp. 259, 273, 19-22 July 2014. doi:10.1109/CSF.2014.26
Abstract: In formal verification, cryptographic messages are often represented by algebraic terms. This abstracts not only from the intricate details of the real cryptography, but also from the details of the non-cryptographic aspects: the actual formatting and structuring of messages. We introduce a new algebraic model to include these details and define a small, simple language to precisely describe message formats. We support fixed-length fields, variable-length fields with offsets, tags, and encodings into smaller alphabets like Base64, thereby covering both classical formats as in TLS and modern XML-based formats. We define two reasonable properties for a set of formats used in a protocol suite. First, each format should be un-ambiguous: any string can be parsed in at most one way. Second, the formats should be pair wise disjoint: a string can be parsed as at most one of the formats. We show how to easily establish these properties for many practical formats. By replacing the formats with free function symbols we obtain an abstract model that is compatible with all existing verification tools. We prove that the abstraction is sound for un-ambiguous, disjoint formats: there is an attack in the concrete message model if there is one in the abstract message model. Finally we present highlights of a practical case study on TLS.
Keywords: XML; cryptography; formal verification; grammars; program compilers; Base64; TLS; XML-based formats; abstract model; algebraic model; algebraic terms; concrete message model; cryptographic messages; fixed-length fields; formal verification; message formats; noncryptographic aspects; parsing problem; sound abstraction; variable-length fields; Abstracts; Algebra; Encoding; Encryption; Law; Protocols; Security protocols; compositional reasoning; formal verification; message formats; soundness (ID#: 15-6041)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6957116&isnumber=6957090

Tzimiropoulos, G.; Alabort-i-Medina, J.; Zafeiriou, S.P.; Pantic, M., “Active Orientation Models for Face Alignment In-the-Wild,” Information Forensics and Security, IEEE Transactions on, vol. 9, no. 12, pp. 2024, 2034, Dec. 2014. doi:10.1109/TIFS.2014.2361018
Abstract: We present Active Orientation Models (AOMs), generative models of facial shape and appearance, which extend the well-known paradigm of Active Appearance Models (AAMs) for the case of generic face alignment under unconstrained conditions. Robustness stems from the fact that the proposed AOMs employ a statistically robust appearance model based on the principal components of image gradient orientations. We show that when incorporated within standard optimization frameworks for AAM learning and fitting, this kernel Principal Component Analysis results in robust algorithms for model fitting. At the same time, the resulting optimization problems maintain the same computational cost. As a result, the main similarity of AOMs with AAMs is the computational complexity. In particular, the project-out version of AOMs is as computationally efficient as the standard project-out inverse compositional algorithm, which is admittedly one of the fastest algorithms for fitting AAMs. We verify experimentally that: 1) AOMs generalize well to unseen variations and 2) outperform all other state-of-the-art AAM methods considered by a large margin. This performance improvement brings AOMs at least in par with other contemporary methods for face alignment. Finally, we provide MATLAB code at http://ibug.doc.ic.ac.uk/resources.
Keywords: computational complexity; face recognition; optimisation; principal component analysis; AAM learning; AAMs; AOMs; MATLAB code; active appearance models; active orientation models; computational complexity; computational cost; face alignment in-the-wild; facial shape; generative models; generic face alignment; image gradient orientations; kernel principal component analysis; model fitting; optimization frameworks; project-out inverse compositional algorithm; unconstrained conditions; Active appearance model; Deformable models; Face; Principal component analysis; Robustness; Shape; Active Appearance Models; Active Orientation Models; Active orientation models; Face alignment; active appearance models; face alignment (ID#: 15-6042)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6914605&isnumber=6953163

Litian Xiao; Mengyuan Li; Ming Gu; Jiaguang Sun, “A Hierarchy Framework on Compositional Verification for PLC Software,” Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on, vol., no., pp. 204, 207, 27-29 June 2014. doi:10.1109/ICSESS.2014.6933545
Abstract: The correctness verification of embedded control software has become an important research topic in embedded system field. The paper analyses the present situation on correctness verification of control software as well as the limitations of existing technologies. In order to the high reliability and high security requirements of control software, the paper proposes a hierarchical framework and architecture of control software (PLC program) verification. The framework combines the technologies of testing, model checking and theorem proving. The paper introduces the construction, flow and key elements of the architecture.
Keywords: control engineering computing; embedded systems; program verification; programmable controllers; theorem proving; PLC program verification; PLC software; compositional verification; control software verification; correctness verification ;embedded control software; embedded system field; hierarchical framework; model checking; security requirements; theorem proving; Computer architecture; Computer bugs; Mathematical model; Model checking; Semantics; Software; PLCsoftware; compositional verification; hierarchy framework; verification architecture (ID#: 15-6043)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6933545&isnumber=6933501

Herber, P., “The RESCUE Approach —Towards Compositional Hardware/Software Co-verification,” High Performance Computing and Communications, 2014 IEEE 6th Intl Symp on Cyberspace Safety and Security, 2014 IEEE 11th Intl Conf on Embedded Software and Syst (HPCC,CSS,ICESS), 2014 IEEE Intl Conf on, vol., no., pp. 721, 724, 20-22 Aug. 2014. doi:10.1109/HPCC.2014.109
Abstract: In the last decades, there has been a lot of work on formal verification techniques for embedded hardware/software systems. The main barriere for the application of these techniques in industrial application is the state-space explosion problem, i.e., The lacking scalability of formal verification. To tackle this problem, we propose a modular verification framework that supports the whole design flow of embedded HW/SW system combining a variety of verification techniques, ranging from formal hardware verification over software verification to system verification. We target the system level design language SystemC, which has become the de facto standard in HW/SW co-design, but severely lacks support for automated and comprehensive verification. To achieve a modular and automatable verification flow, we start with a definition of an intermediate representation for SystemC (SysCIR). Then, we process the SysCIR by a set of modular engines. First, we aim at developing innovative slicing and abstraction engines, which significantly reduce the semantic state space. Second, we aim at providing a set of transformation engines that target a variety of verification tools. In particular, we combine hardware, software and system verification techniques in order to cope with the different models of computation inherently intertwined in embedded HW/SW systems.
Keywords: C language; embedded systems; formal verification; hardware-software codesign; state-space methods; HW/SW codesign; RESCUE approach; SysCIR; SystemC; abstraction engine; automatable verification flow; automated verification; comprehensive verification; de facto standard; design flow; embedded HW/SW system; embedded hardware/software system; formal hardware verification; formal verification technique; hardware/software co-verification; industrial application; innovative slicing; intermediate representation; lacking scalability; modular engine; modular verification framework; software verification; state-space explosion problem; system level design language; system verification technique; transformation engine; verification tool; Computational modeling; Embedded systems; Engines; Hardware; Model checking; Semantics; Formal Verification; Hardware/Software Co-Design (ID#: 15-6044)
URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7056823&isnumber=7056577
 

Note:

Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to news@scienceofsecurity.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.