Language Based Security 2015

	Language Based Security 2015

Application-level security is a key to defending against application-level attacks. Because these applications are typically specified and implemented in programming languages, this area is generally known as "language-based security". Research into language -based security focuses on a range of languages and approaches and is relevant to the Science of Security hard problems of resiliency, metrics, and human behavior. The works cited here were presented between January and August of 2014.

R. Kusters, T. Truderung, B. Beckert, D. Bruns, M. Kirsten and M. Mohr, "A Hybrid Approach for Proving Noninterference of Java Programs," Computer Security Foundations Symposium (CSF), 2015 IEEE 28th, Verona, 2015, pp. 305-319. doi: 10.1109/CSF.2015.28

Abstract: Several tools and approaches for proving non-interference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but over approximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming. In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to over approximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves the verification only of specific functional properties in certain parts of the program, rather than checking more intricate non-interference properties for the whole program. To illustrate the hybrid approach, in a case study we use this approach - along with the fully automatic tool Joana for checking non-interference properties for Java programs and the theorem prover KeY for the verification of Java programs - as well as the CVJ framework proposed by Kuesters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. The CVJ framework allows one to establish cryptographic indistinguishability properties for Java programs by checking (standard) non-interference properties for such programs.

Keywords: Java; program diagnostics; program verification; theorem proving; CVJ framework; Java programs noninterference properties; Joana; KeY theorem prover; automatic analysis; cryptographic privacy properties; e-voting system; functional property verification; hybrid approach; interactive analysis; noninterference property checking; Cryptography; Electronic mail; Electronic voting; Java; Privacy; Standards; code-level cryptographic analysis; language-based security; noninterference; program analysis (ID#: 16-9451)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7243741&isnumber=7243713

A. Askarov, S. Chong and H. Mantel, "Hybrid Monitors for Concurrent Noninterference," Computer Security Foundations Symposium (CSF), 2015 IEEE 28th, Verona, 2015, pp. 137-151. doi: 10.1109/CSF.2015.17

Abstract: Controlling confidential information in concurrent systems is difficult, due to covert channels resulting from interaction between threads. This problem is exacerbated if threads share resources at fine granularity. In this work, we propose a novel monitoring framework to enforce strong information security in concurrent programs. Our monitors are hybrid, combining dynamic and static program analysis to enforce security in a sound and rather precise fashion. In our framework, each thread is guarded by its own local monitor, and there is a single global monitor. We instantiate our monitoring framework to support rely-guarantee style reasoning about the use of shared resources, at the granularity of individual memory locations, and then specialize local monitors further to enforce flow-sensitive progress-sensitive information-flow control. Our local monitors exploit rely-guarantee-style reasoning about shared memory to achieve high precision. Soundness of rely-guarantee-style reasoning is guaranteed by all monitors cooperatively. The global monitor is invoked only when threads synchronize, and so does not needlessly restrict concurrency. We prove that our hybrid monitoring approach enforces a knowledge-based progress-sensitive non-interference security condition.

Keywords: concurrency control; data privacy; inference mechanisms; knowledge based systems; program diagnostics; resource allocation; security of data; storage management; concurrent noninterference; concurrent program; concurrent system; confidential information control; covert channel; dynamic program analysis; flow-sensitive progress-sensitive information-flow control; hybrid monitoring approach; knowledge-based progress-sensitive noninterference security condition; memory location; rely-guarantee style reasoning; resource sharing; security enforcement; shared memory; static program analysis; strong information security; thread interaction; thread synchronization; Cognition; Concurrent computing; Instruction sets; Monitoring; Security; Synchronization; Language-based security; hybrid information-flow monitor; information-flow control for concurrent systems (ID#: 16-9452)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7243730&isnumber=7243713

D. Schoepe and A. Sabelfeld, "Understanding and Enforcing Opacity," Computer Security Foundations Symposium (CSF), 2015 IEEE 28th, Verona, 2015, pp. 539-553. doi: 10.1109/CSF.2015.41

Abstract: This paper puts a spotlight on the specification and enforcement of opacity, a security policy for protecting sensitive properties of system behavior. We illustrate the fine granularity of the opacity policy by location privacy and privacy-preserving aggregation scenarios. We present a general framework for opacity and explore its key differences and formal connections with such well-known information-flow models as non-interference, knowledge-based security, and declassification. Our results are machine-checked and parameterized in the observational power of the attacker, including progress-insensitive, progress-sensitive, and timing-sensitive attackers. We present two approaches to enforcing opacity: a whitebox monitor and a blackbox sampling-based enforcement. We report on experiments with prototypes that utilize state-of-the-art Satisfiability Modulo Theories (SMT) solvers and the random testing tool QuickCheck to establish opacity for the location and aggregation-based scenarios.

Keywords: computability; data privacy; pattern classification; sampling methods; security of data; QuickCheck; SMT; aggregation-based scenarios; blackbox sampling-based enforcement; declassification; formal connections; information-flow models; knowledge-based security; location aggregation-based scenarios; location privacy; opacity policy; privacy-preserving aggregation scenarios; progress-insensitive attackers; progress-sensitive attackers; random testing tool; security policy; sensitive system behavior properties; state-of-the-art satisfiability modulo theories solvers; timing-sensitive attackers; whitebox monitor; Knowledge based systems; Monitoring; Nickel; Privacy; Prototypes; Reactive power; Security; information flow; language-based security (ID#: 16-9453)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7243753&isnumber=7243713

A. Dabrowski, I. Echizen and E. R. Weippl, "Error-Correcting Codes As Source For Decoding Ambiguity," Security and Privacy Workshops (SPW), 2015 IEEE, San Jose, CA, 2015, pp. 99-105. doi: 10.1109/SPW.2015.28

Abstract: Data decoding, format, or language ambiguities have been long known for amusement purposes. Only recently it came to attention that they also pose a security risk. In this paper, we present decoder manipulations based on deliberately caused ambiguities facilitating the error correction mechanisms used in several popular applications. This can be used to encode data in multiple formats or even the same format with different content. Implementation details of the decoder or environmental differences decide which data the decoder locks onto. This leads to different users receiving different content based on a language decoding ambiguity. In general, ambiguity is not desired, however in special cases it can be particularly harmful. Format dissectors can make wrong decisions, e.g. A firewall scans based on one format but the user decodes different harmful content. We demonstrate this behavior with popular barcodes and argue that it can be used to deliver exploits based on the software installed, or use probabilistic effects to divert a small percentage of users to fraudulent sites.

Keywords: bar codes; decoding; encoding; error correction codes; fraud; security of data; barcodes; data decoding; data encoding; decoder manipulations; error correction mechanisms; error-correcting codes; format dissectors; fraudulent sites; language decoding ambiguity; security risk; Decoding; Error correction codes; Security; Software; Standards; Synchronization; Visualization; Barcode; Error Correcting Codes; LangSec; Language Security; Packet-in-Packet; Protocol decoding ambiguity; QR; Steganography (ID#: 16-9454)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7163213&isnumber=7163193

R. Chatterjee, J. Bonneau, A. Juels and T. Ristenpart, "Cracking-Resistant Password Vaults Using Natural Language Encoders," Security and Privacy (SP), 2015 IEEE Symposium on, San Jose, CA, 2015, pp. 481-498. doi: 10.1109/SP.2015.36

Abstract: Password vaults are increasingly popular applications that store multiple passwords encrypted under a single master password that the user memorizes. A password vault can greatly reduce the burden on a user of remembering passwords, but introduces a single point of failure. An attacker that obtains a user's encrypted vault can mount offline brute-force attacks and, if successful, compromise all of the passwords in the vault. In this paper, we investigate the construction of encrypted vaults that resist such offline cracking attacks and force attackers instead to mount online attacks. Our contributions are as follows. We present an attack and supporting analysis showing that a previous design for cracking-resistant vaults -- the only one of which we are aware -- actually degrades security relative to conventional password-based approaches. We then introduce a new type of secure encoding scheme that we call a natural language encoder (NLE). An NLE permits the construction of vaults which, when decrypted with the wrong master password, produce plausible-looking decoy passwords. We show how to build NLEs using existing tools from natural language processing, such as n-gram models and probabilistic context-free grammars, and evaluate their ability to generate plausible decoys. Finally, we present, implement, and evaluate a full, NLE-based cracking-resistant vault system called NoCrack.

Keywords: context-free grammars; cryptography; encoding; natural language processing; probability; NLE; NoCrack; cracking-resistant password vaults; cracking-resistant vault system; encoding scheme security; encrypted vault construction; force attackers; n-gram models; natural language encoders; natural language processing; offline brute-force attacks; offline cracking attacks; password encryption; plausible decoys; plausible-looking decoy passwords; probabilistic context-free grammars; Dictionaries; Encryption; Force; MySpace; Natural languages; Honey Encryption; Language Model; PCFG;  Password Model; Password Vault (ID#: 16-9455)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7163043&isnumber=7163005

M. Anwar and A. Imran, "Access Control for Multi-tenancy in Cloud-Based Health Information Systems," Cyber Security and Cloud Computing (CSCloud), 2015 IEEE 2nd International Conference on, New York, NY, 2015, pp. 104-110. doi: 10.1109/CSCloud.2015.95

Abstract: Cloud technology can be used to support cost effective, scalable, and well-managed healthcare information systems. However, cloud computing, particularly multitenancy, introduces privacy and security issues related to personal health information (PHI). In this paper, we designed ontological models for healthcare workflow and multi-tenancy, and then applied HIPAA requirements on the models to generate HIPAA-compliant access control policies. We used Semantic Web Rule Language (SWRL) to represent access control policies as rules, and we verified the rules with an OWL-DL reasoner. Additionally, we implemented HIPAA security rules through access control policies in a cloud-based simulated healthcare environment. More specifically, we investigated access control policy specification and enforcement for cloud based healthcare information systems using an open source cloud platform, OpenStack. The results manifest HIPAA compliance through authorization policies that are capable of addressing vulnerabilities of multi-tenancy.

Keywords: authorisation; cloud computing; health care; medical information systems; ontologies (artificial intelligence);public domain software; HIPAA-compliant access control policy; OpenStack platform; PHI; authorization policy; cloud computing; cloud technology; cloud-based health information systems; health care information systems; ontological models; open source cloud platform; personal health information; semantic Web rule language; Access control; Cloud computing; Databases; Insurance; Medical services; Ontologies; HIPAA; access control; health cloud; multitenancy; ontological model; openstack (ID#: 16-9456)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7371467&isnumber=7371418

R. N. M. Watson et al., "CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization," Security and Privacy (SP), 2015 IEEE Symposium on, San Jose, CA, 2015, pp. 20-37. doi: 10.1109/SP.2015.9

Abstract: CHERI extends a conventional RISC Instruction-Set Architecture, compiler, and operating system to support fine-grained, capability-based memory protection to mitigate memory-related vulnerabilities in C-language TCBs. We describe how CHERI capabilities can also underpin a hardware-software object-capability model for application compartmentalization that can mitigate broader classes of attack. Prototyped as an extension to the open-source 64-bit BERI RISC FPGA soft-core processor, Free BSD operating system, and LLVM compiler, we demonstrate multiple orders-of-magnitude improvement in scalability, simplified programmability, and resulting tangible security benefits as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate incrementally deployable CHERI-based compartmentalization using several real-world UNIX libraries and applications.

Keywords: data protection; operating systems (computers); program compilers; reduced instruction set computing; software architecture; C-language TCB; CHERI; LLVM compiler; RISC instruction-set architecture; capability-based memory protection; hardware-software object-capability model; hybrid capability-system architecture; operating system; software compartmentalization; Hardware; Kernel; Libraries; Reduced instruction set computing; Registers; Security; CHERI processor; capability system; computer architecture; memory protection; object capabilities; software compartmentalization (ID#: 16-9457)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7163016&isnumber=7163005

Xiaoran Zhu, Yuanmin Xu, Jian Guo, Xi Wu, Huibiao Zhu and Weikai Miao, "Formal Verification of PKMv3 Protocol Using DT-Spin," Theoretical Aspects of Software Engineering (TASE), 2015 International Symposium on, Nanjing, 2015, pp. 71-78. doi: 10.1109/TASE.2015.20

Abstract: WiMax (Worldwide Interoperability for Microwave Access, IEEE 802.16) is a standard-based wireless technology, which uses Privacy Key Management (PKM) protocol to provide authentication and key management. Three versions of PKM protocol have been released and the third version (PKMv3) strengthens the security by enhancing the message management. In this paper, a formal analysis of PKMv3 protocol is presented. Both the subscriber station (SS) and the base station (BS) are modeled as processes in our framework. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK), which are produced by BS. Moreover, the PKMv3 model is constructed through the discrete-time PROMELA (DT-PROMELA) language and the tool DT-Spin implements the PKMv3 model with lifetime. Finally, we simulate communications between SS and BS and some properties are verified, i.e. liveness, succession and message consistency, which are extracted from PKMv3 and specified using Linear Temporal Logic (LTL) formulae and assertions. Our model provides a basis for further verification of PKMv3 protocol with time characteristic.

Keywords: WiMax; authorisation; computer network security; cryptographic protocols; formal verification; message authentication; private key cryptography; temporal logic; AK; BS; DT-PROMELA language; DT-Spin; DT-spin; IEEE 802.16; LTL; PKM protocol; PKMv3 model; PKMv3 protocol; SS;TEK; WiMax; Worldwide Interoperability for Microwave Access; authentication; authorization key; base station; discrete-time PROMELA language; formal verification; linear temporal logic; message management; privacy key management protocol; security; standard-based wireless technology; subscriber station; third version; transmission encryption key; Authentication; Authorization; Encryption; IEEE 802.16 Standard; Protocols; DT-Spin; Discrete-time PROMELA;PKMv3 protocol; modeling; verification (ID#: 16-9458)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7307736&isnumber=7307716

S. Sadki and H. El Bakkali, "An Approach for Privacy Policies Negotiation in Mobile Health-Cloud Environments," Cloud Technologies and Applications (CloudTech), 2015 International Conference on, Marrakech, 2015, pp. 1-6. doi: 10.1109/CloudTech.2015.7336983

Abstract: Mobile technologies continue to improve patients' quality of care. Particularly, with the emergence of Cloud-based mobile services and applications, patients can easily communicate with their physicians and receive the care they deserve. However, due to the increased number of privacy threats in mobile and Cloud computing environments, maximizing patients' control over their data becomes a necessity. Thus, formal languages to express their privacy preferences are needed. Besides, because of the diversity of actors involved in patient's care, conflict among privacy policies can take place. In this paper, we present an approach that aims to resolve the problem of conflicting privacy policies based on a Security Policy Negotiation Framework. The major particularity of our solution is that it considers the patient to be a crucial actor in the negotiation process. The different steps of our approach are illustrated through an example of three conflicting privacy policies with different privacy languages.

Keywords: cloud computing; data privacy; health care ;medical computing; mobile computing; cloud computing; cloud-based mobile services; formal language; mobile health-cloud environment; mobile technology; patient care; privacy policy negotiation; security policy negotiation framework; Cloud computing; Data privacy; Medical services; Mobile communication; Organizations; Privacy; Security; Cloud computing; mobile health; policy negotiation; privacy; privacy policy (ID#: 16-9459)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7336983&isnumber=7336956

H. T. Poon and A. Miri, "An Efficient Conjunctive Keyword and Phase Search Scheme for Encrypted Cloud Storage Systems," Cloud Computing (CLOUD), 2015 IEEE 8th International Conference on, New York City, NY, 2015, pp. 508-515. doi: 10.1109/CLOUD.2015.74

Abstract: There has been increasing interest in the area of privacy-protected searching as industries continue to adopt cloud technologies. Much of the recent efforts have been towards incorporating more advanced searching techniques. Although many have proposed solutions for conjunctive keyword search, it is only recently that researchers began exploring phrase search over encrypted data. In this paper, we present a scheme that incorporates both functionalities. Our solution makes use of symmetric encryption, which provides computational and storage efficiency over schemes based on public key encryption. By considering the statistical properties of natural languages, we were able to design indexes that significantly reduce storage cost when compared to existing solutions. Our solution allows for simple ranking of results and requires a low storage cost while providing document and keyword security. By using both the index and the encrypted documents to performs searches, our scheme is also currently the only phrase search scheme capable of searching for non-indexed keywords.

Keywords: cloud computing; data protection; natural language processing; public key cryptography; storage management; advanced searching techniques; cloud technology; conjunctive keyword search; encrypted cloud storage systems; keyword security; natural languages; phase search scheme; privacy-protected searching; public key encryption; statistical property; storage cost reduction; symmetric encryption; Cloud computing; Encryption; Indexes; Keyword search; Servers; Conjunctive keyword search; Encryption; Phrase search; Privacy; Security (ID#: 16-9460)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7214084&isnumber=7212169

E. M. Songhori, S. U. Hussain, A. R. Sadeghi, T. Schneider and F. Koushanfar, "Tiny Garble: Highly Compressed and Scalable Sequential Garbled Circuits," Security and Privacy (SP), 2015 IEEE Symposium on, San Jose, CA, 2015, pp. 411-428. doi: 10.1109/SP.2015.32

Abstract: We introduce Tiny Garble, a novel automated methodology based on powerful logic synthesis techniques for generating and optimizing compressed Boolean circuits used in secure computation, such as Yao's Garbled Circuit (GC) protocol. Tiny Garble achieves an unprecedented level of compactness and scalability by using a sequential circuit description for GC. We introduce new libraries and transformations, such that our sequential circuits can be optimized and securely evaluated by interfacing with available garbling frameworks. The circuit compactness makes the memory footprint of the garbling operation fit in the processor cache, resulting in fewer cache misses and thereby less CPU cycles. Our proof-of-concept implementation of benchmark functions using Tiny Garble demonstrates a high degree of compactness and scalability. We improve the results of existing automated tools for GC generation by orders of magnitude, for example, Tiny Garble can compress the memory footprint required for 1024-bit multiplication by a factor of 4,172, while decreasing the number of non-XOR gates by 67%. Moreover, with Tiny Garble we are able to implement functions that have never been reported before, such as SHA-3. Finally, our sequential description enables us to design and realize a garbled processor, using the MIPS I instruction set, for private function evaluation. To the best of our knowledge, this is the first scalable emulation of a general purpose processor.

Keywords: logic circuits; logic design; TinyGarble methodology; Yao garbled circuit protocol; compactness degree; compressed Boolean circuits; general purpose processor; instruction set; logic synthesis techniques; private function evaluation; scalability degree; sequential description; sequential garbled circuits; Hardware design languages; Libraries; Logic gates; Optimization; Protocols; Sequential circuits; Wires; Garbled Circuit; Hardware Synthesis; Logic Design; Secure Function Evaluation (ID#: 16-9461)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7163039&isnumber=7163005

A. Vasilateanu and A. Buga, "AsthMate -- Supporting Patient Empowerment through Location-Based Smartphone Applications," Control Systems and Computer Science (CSCS), 2015 20th International Conference on, Bucharest, 2015, pp. 411-417.  doi: 10.1109/CSCS.2015.61

Abstract: The ever changing challenges and pressures to the healthcare domain have introduced the urgency of finding a replacement for traditional systems. Breakthroughs registered by information systems, advances in data storage and processing solutions sustained by the ubiquity of gadgets and an efficient infrastructure for network and services have sustained a shift of medical systems towards digital healthcare. Asth Mate application is an e-health tool for asthma patients, acting as an enabler for patient empowerment. The contributions brought by the application are both to the individual and to the community exposing a web application that allows citizens to check the state of the air for the area they live in. The ongoing implementation can benefit of the advantages of cloud computing solutions in order to ensure a better deployment and data accessibility. However, data privacy is a key aspect for such systems. In consideration of this reason, a proper trade-off between the functionality, data openness and security should be reached.

Keywords: cloud computing; health care; smart phones; Asth Mate application; Web application; asthma patients; cloud computing solutions; data privacy; digital healthcare; e-health tool; information systems; location-based smartphone applications; patient empowerment; Biomedical monitoring; Cloud computing; Collaboration; Diseases; Monitoring; Prototypes; cloud computing; e-health; mobile computing; patient empowerment (ID#: 16-9462)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7168462&isnumber=7168393

S. Daoudagh, F. Lonetti and E. Marchetti, "Assessment of Access Control Systems Using Mutation Testing," TEchnical and LEgal aspects of data pRivacy and SEcurity, 2015 IEEE/ACM 1st International Workshop on, Florence, 2015, pp. 8-13. doi: 10.1109/TELERISE.2015.10

Abstract: In modern pervasive applications, it is important to validate access control mechanisms that are usually defined by means of the standard XACML language. Mutation analysis has been applied on access control policies for measuring the adequacy of a test suite. In this paper, we present a testing framework aimed at applying mutation analysis at the level of the Java based policy evaluation engine. A set of Java based mutation operators is selected and applied to the code of the Policy Decision Point (PDP). A first experiment shows the effectiveness of the proposed framework in assessing the fault detection of XACML test suites and confirms the efficacy of the application of code-based mutation operators to the PDP.

Keywords: Java; authorisation; program diagnostics; program testing; ubiquitous computing; Java based mutation operators; Java based policy evaluation engine; PDP; access control system assessment; code-based mutation operators; fault detection; mutation testing analysis; policy decision point code; standard XACML language; Access control; Engines; Fault detection; Java; Proposals; Sun; Testing (ID#: 16-9463)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7182463&isnumber=7182453

S. Sadki and H. E. Bakkali, "Towards Negotiable Privacy Policies in Mobile Healthcare," Innovative Computing Technology (INTECH), 2015 Fifth International Conference on, Galcia, 2015, pp. 94-99. doi: 10.1109/INTECH.2015.7173478

Abstract: With the increased use of mobile technologies in the health sector, patients are more and more concerned about their privacy protection. Particularly, due to the diversity of actors (physicians, healthcare organizations, Cloud providers...) and the heterogeneity of privacy policies defined by each actor, conflicts among these policies may occur. We believe that negotiation is one of the best techniques for resolving the issue of conflicting privacy policies. From this perspective, we present an approach and algorithm to negotiate privacy policies based on an extension of the bargaining model. Besides, in order to show how our solution can be applied, we present an example of conflicting privacy policies expressed using S4P, a generic language for specifying privacy preferences and policies.

Keywords: data privacy; medical information systems; mobile computing; S4P; bargaining model; generic language; health sector; mobile healthcare; mobile technologies; negotiable privacy policies; privacy policies; privacy preferences; privacy protection; Data privacy; Medical services; Mobile communication; Mobile handsets; Pragmatics; Privacy; Vocabulary; Mobile Healthcare; component; conflicting policies; policy negotiation; privacy; privacy policy language (ID#: 16-9464)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7173478&isnumber=7173359

E. B. Fernandez, N. Yoshioka and H. Washizaki, "Patterns for Security and Privacy in Cloud Ecosystems," Evolving Security and Privacy Requirements Engineering (ESPRE), 2015 IEEE 2nd Workshop on, Ottawa, ON, 2015, pp. 13-18. doi: 10.1109/ESPRE.2015.7330162

Abstract: An ecosystem is the expansion of a software product line architecture to include systems outside the product which interact with the product. We model here the architecture of a cloud-based ecosystem, showing security patterns for its main components. We discuss the value of this type of models.

Keywords: cloud computing; data privacy; security of data; software architecture; cloud ecosystems privacy; cloud ecosystems security; cloud-based ecosystem; security patterns; software product line architecture; Cloud computing; Computer architecture; Ecosystems; Security; Software as a service; Unified modeling language; Virtualization; Software ecosystems; cloud computing; reference architectures; security patterns; systems security (ID#: 16-9465)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7330162&isnumber=7330155

Shaun Shei, L. Marquez Alcaniz, H. Mouratidis, A. Delaney, D. G. Rosado and E. Fernandez-Medina, "Modelling Secure Cloud Systems Based on System Requirements," Evolving Security and Privacy Requirements Engineering (ESPRE), 2015 IEEE 2nd Workshop on, Ottawa, ON, 2015, pp. 19-24. doi: 10.1109/ESPRE.2015.7330163

Abstract: We enhance an existing security governance framework for migrating legacy systems to the cloud by holistically modelling the cloud infrastructure. To achieve this we demonstrate how components of the cloud infrastructure can be identified from existing security requirements models. We further extend the modelling language to capture cloud security requirements through a dual layered view of the cloud infrastructure, where the notions are supported through a running example.

Keywords: cloud computing; security of data; software maintenance; specification languages; cloud infrastructure; cloud security requirements; legacy systems; modelling language; secure cloud system modeling; security governance framework; security requirements models; system requirements; Aging; Analytical models; Cloud computing; Computational modeling; Guidelines; Physical layer; Security (ID#: 16-9466)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7330163&isnumber=7330155

K. Katkalov, K. Stenzel, M. Borek and W. Reif, "Modeling Information Flow Properties with UML," New Technologies, Mobility and Security (NTMS), 2015 7th International Conference on, Paris, 2015, pp. 1-5. doi: 10.1109/NTMS.2015.7266507

Abstract: Providing guarantees regarding the privacy of sensitive information in a distributed system consisting of mobile apps and services is a challenging task. Our IFlow approach allows the model-driven development of such systems, as well as the automatic generation of code and a formal model. In this paper, we introduce modeling guidelines for the design of intuitive, flexible and expressive information flow properties with UML. Further, we show how these properties can be guaranteed using a combination of automatic language-based information flow control and model-based interactive verification.

Keywords: codes; formal verification; mobile computing; telecommunication control; telecommunication services; IFlow approach; UML; Unified Modeling Language; automatic language; distributed system; information flow control; information flow properties; mobile apps; model-based interactive verification; sensitive information; Analytical models; Androids; Java; Mobile communication; Security; Unified modeling language; information flow; model-driven software development; privacy (ID#: 16-9467)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7266507&isnumber=7266450

H. Ulusoy, M. Kantarcioglu, B. Thuraisingham and L. Khan, "Honeypot Based Unauthorized Data Access Detection in MapReduce Systems," Intelligence and Security Informatics (ISI), 2015 IEEE International Conference on, Baltimore, MD, 2015, pp. 126-131. doi: 10.1109/ISI.2015.7165951

Abstract: The data processing capabilities of MapReduce systems pioneered with the on-demand scalability of cloud computing have enabled the Big Data revolution. However, the data controllers/owners worried about the privacy and accountability impact of storing their data in the cloud infrastructures as the existing cloud computing solutions provide very limited control on the underlying systems. The intuitive approach - encrypting data before uploading to the cloud - is not applicable to MapReduce computation as the data analytics tasks are ad-hoc defined in the MapReduce environment using general programming languages (e.g, Java) and homomorphic encryption methods that can scale to big data do not exist. In this paper, we address the challenges of determining and detecting unauthorized access to data stored in MapReduce based cloud environments. To this end, we introduce alarm raising honeypots distributed over the data that are not accessed by the authorized MapReduce jobs, but only by the attackers and/or unauthorized users. Our analysis shows that unauthorized data accesses can be detected with reasonable performance in MapReduce based cloud environments.

Keywords: Big Data; cloud computing; cryptography; data analysis; data privacy; parallel processing; Big Data revolution; MapReduce systems; cloud computing; data analytics tasks; data encryption; data processing capabilities; general programming languages; homomorphic encryption methods; honeypot; on-demand scalability; privacy; unauthorized data access detection; Big data; Cloud computing; Computational modeling; Cryptography; Data models; Distributed databases (ID#: 16-9468)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7165951&isnumber=7165923

D. Gurov, P. Laud and R. Guanciale, "Privacy Preserving Business Process Matching," Privacy, Security and Trust (PST), 2015 13th Annual Conference on, Izmir, 2015, pp. 36-43. doi: 10.1109/PST.2015.7232952

Abstract: Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises. In this paper we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm in the programming language SecreC, executing on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

Keywords: automata theory; business process re-engineering; data privacy; open systems; security of data; virtual enterprises; SecreC; Sharemind platform; business process matching; information privacy; interoperability; programming language; secure multiparty computation; service automata; virtual enterprise; Automata; Business; Collaboration; Guidelines; Privacy; System recovery; Weight measurement (ID#: 16-9469)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7232952&isnumber=7232940

J. Caramujo and A. M. Rodrigues Da Silva, "Analyzing Privacy Policies Based on a Privacy-Aware Profile: The Facebook and LinkedIn Case Studies," Business Informatics (CBI), 2015 IEEE 17th Conference on, Lisbon, 2015, pp. 77-84. doi: 10.1109/CBI.2015.44

Abstract: The regular use of social networking websites and applications encompasses the collection and retention of personal and very often sensitive information about users. This information needs to remain private and each social network owns a privacy policy that describes in-depth how users' information is managed and disclosed. Problems arise when the development of new systems and applications includes an integration with social networks. The lack of clear understanding and a precise mechanism to enforce the statements described in privacy policies can compromise the development and adaptation of these statements. This paper proposes the extension and validation of a UML profile for privacy-aware systems. The goal of this approach is to provide a better understanding of the different privacy-related requirements for improving privacy policies enforcement when developing systems or applications integrated with social networks. Additionally, to illustrate the potential of this profile, the paper presents and discusses its application with two real world case studies - the Facebook and Linked In policies - which are well structured and represented through two respective Excel files.

Keywords: Unified Modeling Language; computer network security; data privacy; information management; social networking (online);Excel file; Facebook; LinkedIn; UML profile; privacy aware profile; privacy aware system; privacy profile analysis; social networking Websites; user information management; Business; Conferences; Informatics; Facebook; LinkedIn; Privacy; Requirements; System; UML profile; integration (ID#: 16-9470)

URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7264718&isnumber=7264698

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.