Visible to the public Biblio

Found 2348 results

Filters: Keyword is privacy  [Clear All Filters]
2017-11-03
Liao, K., Zhao, Z., Doupe, A., Ahn, G. J..  2016.  Behind closed doors: measurement and analysis of CryptoLocker ransoms in Bitcoin. 2016 APWG Symposium on Electronic Crime Research (eCrime). :1–13.

Bitcoin, a decentralized cryptographic currency that has experienced proliferating popularity over the past few years, is the common denominator in a wide variety of cybercrime. We perform a measurement analysis of CryptoLocker, a family of ransomware that encrypts a victim's files until a ransom is paid, within the Bitcoin ecosystem from September 5, 2013 through January 31, 2014. Using information collected from online fora, such as reddit and BitcoinTalk, as an initial starting point, we generate a cluster of 968 Bitcoin addresses belonging to CryptoLocker. We provide a lower bound for CryptoLocker's economy in Bitcoin and identify 795 ransom payments totalling 1,128.40 BTC (\$310,472.38), but show that the proceeds could have been worth upwards of \$1.1 million at peak valuation. By analyzing ransom payment timestamps both longitudinally across CryptoLocker's operating period and transversely across times of day, we detect changes in distributions and form conjectures on CryptoLocker that corroborate information from previous efforts. Additionally, we construct a network topology to detail CryptoLocker's financial infrastructure and obtain auxiliary information on the CryptoLocker operation. Most notably, we find evidence that suggests connections to popular Bitcoin services, such as Bitcoin Fog and BTC-e, and subtle links to other cybercrimes surrounding Bitcoin, such as the Sheep Marketplace scam of 2013. We use our study to underscore the value of measurement analyses and threat intelligence in understanding the erratic cybercrime landscape.

Gambino, Andrew, Kim, Jinyoung, Sundar, S. Shyam, Ge, Jun, Rosson, Mary Beth.  2016.  User Disbelief in Privacy Paradox: Heuristics That Determine Disclosure. Proceedings of the 2016 CHI Conference Extended Abstracts on Human Factors in Computing Systems. :2837–2843.
We conducted a series of in-depth focus groups wherein users provided rationales for their own online privacy behaviors. Our data suggest that individuals often take action with little thought or evaluation, even showing surprise when confronted with their own behaviors. Our analysis yielded a battery of cognitive heuristics, i.e., mental shortcuts / rules of thumb, that users seem to employ when they disclose or withhold information at the spur of the moment. A total of 4 positive heuristics (promoting disclosure) and 4 negative heuristics (inhibiting disclosure) were discovered. An understanding of these heuristics can be valuable for designing interfaces that promote secure and trustworthy computing.
2017-10-25
Chowdhury, Soumyadeb, Ferdous, Md Sadek, Jose, Joemon M.  2016.  Exploring Lifelog Sharing and Privacy. Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing: Adjunct. :553–558.

The emphasis on exhaustive passive capturing of images using wearable cameras like Autographer, which is often known as lifelogging has brought into foreground the challenge of preserving privacy, in addition to presenting the vast amount of images in a meaningful way. In this paper, we present a user-study to understand the importance of an array of factors that are likely to influence the lifeloggers to share their lifelog images in their online circle. The findings are a step forward in the emerging area intersecting HCI, and privacy, to help in exploring design directions for privacy mediating techniques in lifelogging applications.

Kaizer, Andrew J., Gupta, Minaxi.  2016.  Towards Automatic Identification of JavaScript-oriented Machine-Based Tracking. Proceedings of the 2016 ACM on International Workshop on Security And Privacy Analytics. :33–40.

Machine-based tracking is a type of behavior that extracts information on a user's machine, which can then be used for fingerprinting, tracking, or profiling purposes. In this paper, we focus on JavaScript-oriented machine-based tracking as JavaScript is widely accessible in all browsers. We find that coarse features related to JavaScript access, cookie access, and URL length subdomain information can perform well in creating a classifier that can identify these machine-based trackers with 97.7% accuracy. We then use the classifier on real-world datasets based on 30-minute website crawls of different types of websites – including websites that target children and websites that target a popular audience – and find 85%+ of all websites utilize machine-based tracking, even when they target a regulated group (children) as their primary audience.

Perera, Charith, McCormick, Ciaran, Bandara, Arosha K., Price, Blaine A., Nuseibeh, Bashar.  2016.  Privacy-by-Design Framework for Assessing Internet of Things Applications and Platforms. Proceedings of the 6th International Conference on the Internet of Things. :83–92.

The Internet of Things (IoT) systems are designed and developed either as standalone applications from the ground-up or with the help of IoT middleware platforms. They are designed to support different kinds of scenarios, such as smart homes and smart cities. Thus far, privacy concerns have not been explicitly considered by IoT applications and middleware platforms. This is partly due to the lack of systematic methods for designing privacy that can guide the software development process in IoT. In this paper, we propose a set of guidelines, a privacy by-design framework, that can be used to assess privacy capabilities and gaps of existing IoT applications as well as middleware platforms. We have evaluated two open source IoT middleware platforms, namely OpenIoT and Eclipse SmartHome, to demonstrate how our framework can be used in this way.

Mense, Alexander, Steger, Sabrina, Jukic-Sunaric, Dragan, Mészáros, András, Sulek, Matthias.  2016.  Open Source Based Privacy-Proxy to Restrain Connectivity of Mobile Apps. Proceedings of the 14th International Conference on Advances in Mobile Computing and Multi Media. :284–287.

Mobile Devices are part of our lives and we store a lot of private information on it as well as use services that handle sensitive information (e.g. mobile health apps). Whenever users install an application on their smartphones they have to decide whether to trust the applications and share private and sensitive data with at least the developer-owned services. But almost all modern apps not only transmit data to the developer owned servers but also send information to advertising-, analyzing and tracking partners. This paper presents an approach for a "privacy- proxy" which enables to filter unwanted data traffic to third party services without installing additional applications on the smartphone. It is based on a firewall using a black list of tracking- and analyzing networks which is automatically updated on a daily basis. The proof of concept has been implemented with open source components on a Raspberry Pi.

Ferdous, Md Sadek, Chowdhury, Soumyadeb, Jose, Joemon M.  2016.  Privacy Threat Model in Lifelogging. Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing: Adjunct. :576–581.

The lifelogging activity enables a user, the lifelogger, to passively capture multimodal records from a first-person perspective and ultimately create a visual diary encompassing every possible aspect of her life with unprecedented details. In recent years it has gained popularity among different groups of users. However, the possibility of ubiquitous presence of lifelogging devices especially in private spheres has raised serious concerns with respect to personal privacy. Different practitioners and active researchers in the field of lifelogging have analysed the issue of privacy in lifelogging and proposed different mitigation strategies. However, none of the existing works has considered a well-defined privacy threat model in the domain of lifelogging. Without a proper threat model, any analysis and discussion of privacy threats in lifelogging remains incomplete. In this paper we aim to fill in this gap by introducing a first-ever privacy threat model identifying several threats with respect to lifelogging. We believe that the introduced threat model will be an essential tool and will act as the basis for any further research within this domain.

2017-10-19
Knote, Robin, Baraki, Harun, Söllner, Matthias, Geihs, Kurt, Leimeister, Jan Marco.  2016.  From Requirement to Design Patterns for Ubiquitous Computing Applications. Proceedings of the 21st European Conference on Pattern Languages of Programs. :26:1–26:11.
Ubiquitous Computing describes a concept where computing appears around us at any time and any location. Respective systems rely on context-sensitivity and adaptability. This means that they constantly collect data of the user and his context to adapt its functionalities to certain situations. Hence, the development of Ubiquitous Computing systems is not only a technical issue and must be considered from a privacy, legal and usability perspective, too. This indicates a need for several experts from different disciplines to participate in the development process, mentioning requirements and evaluating design alternatives. In order to capture the knowledge of these interdisciplinary teams to make it reusable for similar problems, a pattern logic can be applied. In the early phase of a development project, requirement patterns are used to describe recurring requirements for similar problems, whereas in a more advanced development phase, design patterns are deployed to find a suitable design for recurring requirements. However, existing literature does not give sufficient insights on how both concepts are related and how the process of deriving design patterns from requirements (patterns) appears in practice. In our work, we give insights on how trust-related requirements for Ubiquitous Computing applications evolve to interdisciplinary design patterns. We elaborate on a six-step process using an example requirement pattern. With this contribution, we shed light on the relation of interdisciplinary requirement and design patterns and provide experienced practitioners and scholars regarding UC application development a way for systematic and effective pattern utilization.
Zhang, Chenwei, Xie, Sihong, Li, Yaliang, Gao, Jing, Fan, Wei, Yu, Philip S..  2016.  Multi-source Hierarchical Prediction Consolidation. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :2251–2256.
In big data applications such as healthcare data mining, due to privacy concerns, it is necessary to collect predictions from multiple information sources for the same instance, with raw features being discarded or withheld when aggregating multiple predictions. Besides, crowd-sourced labels need to be aggregated to estimate the ground truth of the data. Due to the imperfection caused by predictive models or human crowdsourcing workers, noisy and conflicting information is ubiquitous and inevitable. Although state-of-the-art aggregation methods have been proposed to handle label spaces with flat structures, as the label space is becoming more and more complicated, aggregation under a label hierarchical structure becomes necessary but has been largely ignored. These label hierarchies can be quite informative as they are usually created by domain experts to make sense of highly complex label correlations such as protein functionality interactions or disease relationships. We propose a novel multi-source hierarchical prediction consolidation method to effectively exploits the complicated hierarchical label structures to resolve the noisy and conflicting information that inherently originates from multiple imperfect sources. We formulate the problem as an optimization problem with a closed-form solution. The consolidation result is inferred in a totally unsupervised, iterative fashion. Experimental results on both synthetic and real-world data sets show the effectiveness of the proposed method over existing alternatives.
Grushka - Cohen, Hagit, Sofer, Oded, Biller, Ofer, Shapira, Bracha, Rokach, Lior.  2016.  CyberRank: Knowledge Elicitation for Risk Assessment of Database Security. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :2009–2012.
Security systems for databases produce numerous alerts about anomalous activities and policy rule violations. Prioritizing these alerts will help security personnel focus their efforts on the most urgent alerts. Currently, this is done manually by security experts that rank the alerts or define static risk scoring rules. Existing solutions are expensive, consume valuable expert time, and do not dynamically adapt to changes in policy. Adopting a learning approach for ranking alerts is complex due to the efforts required by security experts to initially train such a model. The more features used, the more accurate the model is likely to be, but this will require the collection of a greater amount of user feedback and prolong the calibration process. In this paper, we propose CyberRank, a novel algorithm for automatic preference elicitation that is effective for situations with limited experts' time and outperforms other algorithms for initial training of the system. We generate synthetic examples and annotate them using a model produced by Analytic Hierarchical Processing (AHP) to bootstrap a preference learning algorithm. We evaluate different approaches with a new dataset of expert ranked pairs of database transactions, in terms of their risk to the organization. We evaluated using manual risk assessments of transaction pairs, CyberRank outperforms all other methods for cold start scenario with error reduction of 20%.
Cerf, Sophie, Robu, Bogdan, Marchand, Nicolas, Boutet, Antoine, Primault, Vincent, Mokhtar, Sonia Ben, Bouchenak, Sara.  2016.  Toward an Easy Configuration of Location Privacy Protection Mechanisms. Proceedings of the Posters and Demos Session of the 17th International Middleware Conference. :11–12.

The widespread adoption of Location-Based Services (LBSs) has come with controversy about privacy. While leveraging location information leads to improving services through geo-contextualization, it rises privacy concerns as new knowledge can be inferred from location records, such as home/work places, habits or religious beliefs. To overcome this problem, several Location Privacy Protection Mechanisms (LPPMs) have been proposed in the literature these last years. However, every mechanism comes with its own configuration parameters that directly impact the privacy guarantees and the resulting utility of protected data. In this context, it can be difficult for a non-expert system designer to choose appropriate configuration parameters to use according to the expected privacy and utility. In this paper, we present a framework enabling the easy configuration of LPPMs. To achieve that, our framework performs an offline, in-depth automated analysis of LPPMs to provide the formal relationship between their configuration parameters and both privacy and the utility metrics. This framework is modular: by using different metrics, a system designer is able to fine-tune her LPPM according to her expected privacy and utility guarantees (i.e., the guarantee itself and the level of this guarantee). To illustrate the capability of our framework, we analyse Geo-Indistinguishability (a well known differentially private LPPM) and we provide the formal relationship between its &epsis; configuration parameter and two privacy and utility metrics.

Dupree, Janna Lynn, Devries, Richard, Berry, Daniel M., Lank, Edward.  2016.  Privacy Personas: Clustering Users via Attitudes and Behaviors Toward Security Practices. Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems. :5228–5239.
A primary goal of research in usable security and privacy is to understand the differences and similarities between users. While past researchers have clustered users into different groups, past categories of users have proven to be poor predictors of end-user behaviors. In this paper, we perform an alternative clustering of users based on their behaviors. Through the analysis of data from surveys and interviews of participants, we identify five user clusters that emerge from end-user behaviors-Fundamentalists, Lazy Experts, Technicians, Amateurs and the Marginally Concerned. We examine the stability of our clusters through a survey-based study of an alternative sample, showing that clustering remains consistent. We conduct a small-scale design study to demonstrate the utility of our clusters in design. Finally, we argue that our clusters complement past work in understanding privacy choices, and that our categorization technique can aid in the design of new computer security technologies.
2017-10-18
Küçük, Kubilay Ahmet, Paverd, Andrew, Martin, Andrew, Asokan, N., Simpson, Andrew, Ankele, Robin.  2016.  Exploring the Use of Intel SGX for Secure Many-Party Applications. Proceedings of the 1st Workshop on System Software for Trusted Execution. :5:1–5:6.

The theoretical construct of a Trusted Third Party (TTP) has the potential to solve many security and privacy challenges. In particular, a TTP is an ideal way to achieve secure multiparty computation—a privacy-enhancing technique in which mutually distrusting participants jointly compute a function over their private inputs without revealing these inputs. Although there exist cryptographic protocols to achieve this, their performance often limits them to the two-party case, or to a small number of participants. However, many real-world applications involve thousands or tens of thousands of participants. Examples of this type of many-party application include privacy-preserving energy metering, location-based services, and mobile network roaming. Challenging the notion that a trustworthy TTP does not exist, recent research has shown how trusted hardware and remote attestation can be used to establish a sufficient level of assurance in a real system such that it can serve as a trustworthy remote entity (TRE). We explore the use of Intel SGX, the most recent and arguably most promising trusted hardware technology, as the basis for a TRE for many-party applications. Using privacy-preserving energy metering as a case study, we design and implement a prototype TRE using SGX, and compare its performance to a previous system based on the Trusted Platform Module (TPM). Our results show that even without specialized optimizations, SGX provides comparable performance to the optimized TPM system, and therefore has significant potential for large-scale many-party applications.

2017-10-10
Marxer, Claudio, Scherb, Christopher, Tschudin, Christian.  2016.  Access-Controlled In-Network Processing of Named Data. Proceedings of the 3rd ACM Conference on Information-Centric Networking. :77–82.

In content-based security, encrypted content as well as wrapped access keys are made freely available by an Information Centric Network: Only those clients which are able to unwrap the encryption key can access the protected content. In this paper we extend this model to computation chains where derived data (e.g. produced by a Named Function Network) also has to comply to the content-based security approach. A central problem to solve is the synchronized on-demand publishing of encrypted results and wrapped keys as well as defining the set of consumers which are authorized to access the derived data. In this paper we introduce "content-attendant policies" and report on a running prototype that demonstrates how to enforce data owner-defined access control policies despite fully decentralized and arbitrarily long computation chains.

Cummings, Rachel, Ligett, Katrina, Radhakrishnan, Jaikumar, Roth, Aaron, Wu, Zhiwei Steven.  2016.  Coordination Complexity: Small Information Coordinating Large Populations. Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science. :281–290.

We initiate the study of a quantity that we call coordination complexity. In a distributed optimization problem, the information defining a problem instance is distributed among n parties, who need to each choose an action, which jointly will form a solution to the optimization problem. The coordination complexity represents the minimal amount of information that a centralized coordinator, who has full knowledge of the problem instance, needs to broadcast in order to coordinate the n parties to play a nearly optimal solution. We show that upper bounds on the coordination complexity of a problem imply the existence of good jointly differentially private algorithms for solving that problem, which in turn are known to upper bound the price of anarchy in certain games with dynamically changing populations. We show several results. We fully characterize the coordination complexity for the problem of computing a many-to-one matching in a bipartite graph. Our upper bound in fact extends much more generally to the problem of solving a linearly separable convex program. We also give a different upper bound technique, which we use to bound the coordination complexity of coordinating a Nash equilibrium in a routing game, and of computing a stable matching.

2017-10-04
Hayes, Jamie, Troncoso, Carmela, Danezis, George.  2016.  TASP: Towards Anonymity Sets That Persist. Proceedings of the 2016 ACM on Workshop on Privacy in the Electronic Society. :177–180.

Anonymous communication systems are vulnerable to long term passive "intersection attacks". Not all users of an anonymous communication system will be online at the same time, this leaks some information about who is talking to who. A global passive adversary observing all communications can learn the set of potential recipients of a message with more and more confidence over time. Nearly all deployed anonymous communication tools offer no protection against such attacks. In this work, we introduce TASP, a protocol used by an anonymous communication system that mitigates intersection attacks by intelligently grouping clients together into anonymity sets. We find that with a bandwidth overhead of just 8% we can dramatically extend the time necessary to perform a successful intersection attack.

2017-10-03
Chattopadhyay, Eshan, Goyal, Vipul, Li, Xin.  2016.  Non-malleable Extractors and Codes, with Their Many Tampered Extensions. Proceedings of the Forty-eighth Annual ACM Symposium on Theory of Computing. :285–298.

Randomness extractors and error correcting codes are fundamental objects in computer science. Recently, there have been several natural generalizations of these objects, in the context and study of tamper resilient cryptography. These are seeded non-malleable extractors, introduced by Dodis and Wichs; seedless non-malleable extractors, introduced by Cheraghchi and Guruswami; and non-malleable codes, introduced by Dziembowski, Pietrzak and Wichs. Besides being interesting on their own, they also have important applications in cryptography, e.g, privacy amplification with an active adversary, explicit non-malleable codes etc, and often have unexpected connections to their non-tampered analogues. However, the known constructions are far behind their non-tampered counterparts. Indeed, the best known seeded non-malleable extractor requires min-entropy rate at least 0.49; while explicit constructions of non-malleable two-source extractors were not known even if both sources have full min-entropy, and was left as an open problem by Cheraghchi and Guruswami. In this paper we make progress towards solving the above problems and other related generalizations. Our contributions are as follows. (1) We construct an explicit seeded non-malleable extractor for polylogarithmic min-entropy. This dramatically improves all previous results and gives a simpler 2-round privacy amplification protocol with optimal entropy loss, matching the best known result. In fact, we construct more general seeded non-malleable extractors (that can handle multiple adversaries) which were used in the recent construction of explicit two-source extractors for polylogarithmic min-entropy. (2) We construct the first explicit non-malleable two-source extractor for almost full min-entropy thus resolving the open question posed by Cheraghchi and Guruswami. (3) We motivate and initiate the study of two natural generalizations of seedless non-malleable extractors and non-malleable codes, where the sources or the codeword may be tampered many times. By using the connection found by Cheraghchi and Guruswami and providing efficient sampling algorithms, we obtain the first explicit non-malleable codes with tampering degree t, with near optimal rate and error. We call these stronger notions one-many and many-manynon-malleable codes. This provides a stronger information theoretic analogue of a primitive known as continuous non-malleable codes. Our basic technique used in all of our constructions can be seen as inspired, in part, by the techniques previously used to construct cryptographic non-malleable commitments.

2017-09-27
Bateman, Scott, Gutwin, Carl.  2016.  (The Lack of) Privacy Concerns with Sharing Web Activity at Work and the Implications for Collaborative Search. Proceedings of the 2016 ACM on Conference on Human Information Interaction and Retrieval. :43–52.
Collaborative information seeking frequently occurs in an opportunistic and loosely-coupled fashion that is supported by awareness of others' activities on the web. Automatically sharing traces of information about web activity could substantially improve these collaborative information tasks, but conventional wisdom suggests that people are very reluctant to share information about web usage. Because work settings have different rules and practices about privacy, we carried out the first systematic study of people's privacy concerns about sharing web activity within workgroups. To provide a better understanding of privacy concerns about sharing web activity at work, we conducted a two-week diary study with 18 participants. Our study system asked participants to report on their search tasks and privacy concerns. Surprisingly, our results showed that people have little concern about sharing the majority of their activities with their work colleagues, and had even fewer concerns with sharing work-related activities. Our results provide new insights into the possibilities of sharing web activities within workgroups, and provide evidence that tools based on automatic sharing of awareness information can be feasible.
2017-09-26
Papadopoulos, Georgios Z., Gallais, Antoine, Schreiner, Guillaume, Noël, Thomas.  2016.  Importance of Repeatable Setups for Reproducible Experimental Results in IoT. Proceedings of the 13th ACM Symposium on Performance Evaluation of Wireless Ad Hoc, Sensor, & Ubiquitous Networks. :51–59.

Performance analysis of newly designed solutions is essential for efficient Internet of Things and Wireless Sensor Network (WSN) deployments. Simulation and experimental evaluation practices are vital steps for the development process of protocols and applications for wireless technologies. Nowadays, the new solutions can be tested at a very large scale over both simulators and testbeds. In this paper, we first discuss the importance of repeatable experimental setups for reproducible performance evaluation results. To this aim, we present FIT IoT-LAB, a very large-scale and experimental testbed, i.e., consists of 2769 low-power wireless devices and 127 mobile robots. We then demonstrate through a number of experiments conducted on FIT IoT-LAB testbed, how to conduct meaningful experiments under real-world conditions. Finally, we discuss to what extent results obtained from experiments could be considered as scientific, i.e., reproducible by the community.

Lavanya, Natarajan.  2016.  Lightweight Authentication for COAP Based IOT. Proceedings of the 6th International Conference on the Internet of Things. :167–168.

Security of Constrained application protocol(COAP) used instead of HTTP in Internet of Thing s(IoT) is achieved using DTLS which uses the Internet key exchange protocol for key exchange and management. In this work a novel key exchange and authentication protocol is proposed. CLIKEv2 protcol is a certificate less and light weight version of the existing protocol. The protocol design is tested with the formal protcol verification tool Scyther, where no named attacks are identified for the propsed protocol. Compared to the existing IKE protocol the CLIKEv2 protocol reduces the computation time, key sizes and ultimately reduces energy consumption.

Padon, Oded, Immerman, Neil, Shoham, Sharon, Karbyshev, Aleksandr, Sagiv, Mooly.  2016.  Decidability of Inferring Inductive Invariants. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. :217–231.

Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols. This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.

Kwon, Youngjin, Dunn, Alan M., Lee, Michael Z., Hofmann, Owen S., Xu, Yuanzhong, Witchel, Emmett.  2016.  Sego: Pervasive Trusted Metadata for Efficiently Verified Untrusted System Services. Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. :277–290.

Sego is a hypervisor-based system that gives strong privacy and integrity guarantees to trusted applications, even when the guest operating system is compromised or hostile. Sego verifies operating system services, like the file system, instead of replacing them. By associating trusted metadata with user data across all system devices, Sego verifies system services more efficiently than previous systems, especially services that depend on data contents. We extensively evaluate Sego's performance on real workloads and implement a kernel fault injector to validate Sego's file system-agnostic crash consistency and recovery protocol.

Gleissenthall, Klaus v., Bjørner, Nikolaj, Rybalchenko, Andrey.  2016.  Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. :599–613.

Parallel and distributed systems rely on intricate protocols to manage shared resources and synchronize, i.e., to manage how many processes are in a particular state. Effective verification of such systems requires universally quantification to reason about parameterized state and cardinalities tracking sets of processes, messages, failures to adequately capture protocol logic. In this paper we present Tool, an automatic invariant synthesis method that integrates cardinality-based reasoning and universal quantification. The resulting increase of expressiveness allows Tool to verify, for the first time, a representative collection of intricate parameterized protocols.

Jebadurai, N. Immanuel, Gupta, Himanshu.  2016.  Automated Verification in Cryptography System. Proceedings of the Second International Conference on Information and Communication Technology for Competitive Strategies. :2:1–2:5.

Cryptographic protocols and algorithms are the strength of digital era in which we are living. Unluckily, the security of many confidential information and credentials has been compromised due to ignorance of required security services. As a result, various attacks have been introduced by talented attackers and many security issues like as financial loss, violations of personal privacy, and security threats to democracy. This research paper provides the secure design and architecture of cryptographic protocols and expedites the authentication of cryptographic system. Designing and developing a secure cryptographic system is like a game in which designer or developer tries to maintain the security while attacker tries to penetrate the security features to perform successful attack.

Mikami, Kei, Ando, Daisuke, Kaneko, Kunitake, Teraoka, Fumio.  2016.  Verification of a Multi-Domain Authentication and Authorization Infrastructure Yamata-no-Orochi. Proceedings of the 11th International Conference on Future Internet Technologies. :69–75.

Yamata-no-Orochi is an authentication and authorization infrastructure across multiple service domains and provides Internet services with unified authentication and authorization mechanisms. In this paper, Yamata-no-Orochi is incorporated into a video distribution system to verify its general versatility as a multi-domain authentication and authorization infrastructure for Internet services. This paper also reduces the authorization time of Yamata-no-Orochi to fulfill the processing time constrains of the video distribution system. The evaluation results show that all the authentication and authorization processes work correctly and the performance of Yamata-no-Orochi is practical for the video distribution system.