Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging task even for experienced administrators. In this paper, we set out to address this pain point by proposing Restricter , which automatically tightens each (permit) policy rule of a policy with respect to an access log, which captures some already exercised access requests and their corresponding access decisions ( i.e. , allow or deny). Restricter achieves policy tightening by reducing the number of access requests permitted by a policy rule without sacrificing the functionality of the underlying system it is regulating. We implement Restricter for Amazon’s Cedar policy language and demonstrate its effectiveness through two realistic case studies.

WPA3-Personal introduced the stateful Simultane-ous Authentication of Equals (SAE) handshake protocol to achieve forward secrecy and resistance to passphrase guessing attacks during Wi-Fi connection bootstrapping, guarantees that are lacking in WPA2-Personal. However, the initial design of WPA3-Personal with SAE was susceptible to connection downgrade and denial-of-service (DoS) attacks. The current, enhanced version introduces mechanisms to mitigate these vulnerabilities. Enabling these security-enhancing mechanisms, however, results in a variable-structured, context-sensitive packet format that can be challenging to parse and interpret correctly. Misparsing SAE handshake packets can negatively impact Wi-Fi protocol security. To uncover SAE handshake packet misparsing in commercial-off-the-shelf (COTS) Wi-Fi access points (APs), we present Saecred,a packet-structure-guided, SAE-state-aware black-box fuzzer. Saecredreduces the underlying problem of misparsing discovery to a two-dimensional search problem, where the dimensions are the packet structure and the underlying SAE protocol state. It solves this search problem by combining Iterative Deepening Search (IDS) with a context-sensitive grammar-based fuzzing approach, where the latter relies on a Syntax-Guided Synthesis (SyGuS) solver. Saecred'seffectiveness is demonstrated by evaluating it on 6 COTS APs and the widely used open-source hostapd. Our evaluation discovered several instances of 4 classes of bugs. Bugs in two of these classes violate the two fundamental guarantees SAE expects to achieve (i.e., resistance to downgrade and DoS attacks). We reported our findings to the relevant stakeholders, which resulted in patches and security advisories.

This paper analyzes the Embedded SIM card's Machine-to-Machine Remote Provisioning Protocol's (eSIM M2M RSP) design. The eSIM M2M RSP simplifies 5G connectivity for IoT devices by securely delivering connection bootstrapping information over the air without human intervention. As IoT adoption with 5G connectivity surges, the eSIM infrastructure must handle a growing number of concurrent remote SIM provisioning requests. The statefulness and shared states of the RSP make it challenging and error-prone to implement concurrency without data races. The GSMA eSIM standard does not explicitly define any atomicity assumptions required for concurrent execution. A formal analysis of the standard-prescribed M2M RSP design reveals that explicit atomicity assumptions are necessary; without them, 31 data races can violate key invariants. During the responsible disclosure process, discussions with the standards body revealed that the M2M RSP design relies on unstated and implicit atomicity assumptions. However, we find that the standard prescribed implicit assumptions are not strong enough to maintain all the invariants. The identified race conditions can be exploited by third-party eSIM management platforms to defraud network operators. To mitigate these risks, we developed a fine-grained synchronization mechanism that we formally verified for correctness and empirically evaluated for performance. Empirical evaluations show that our synchronization mechanism ensures correctness while outperforming a baseline with a 6× speed up.

This paper proposes Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations. Proteus maintains its budget awareness by generating test cases (i.e., each being a sequence of protocol messages) that are not only meaningful (i.e., the test case mostly follows the desirable protocol flow except for some controlled deviations) but also have a high probability of violating the desirable properties. To demonstrate its effectiveness, we evaluated Proteus in two different protocol implementations, namely 4G LTE and BLE, across 23 consumer devices (11 for 4G LTE and 12 for BLE). Proteus discovered 25 unique issues, including 112 instances. Affected vendors have positively acknowledged 14 vulnerabilities through 5 CVEs.

We present our experience of formally verifying the desired security properties of the Uptane over-the-air (OTA) software update framework against a set of applicable threat models. Uptane is gaining traction in the automobile industry and is widely considered the next de-facto standard for OTA automobile software updates. The security of Uptane is of utmost importance because modern automobiles rely on software for their safety-critical functionalities and, especially, require OTA software updates to add new safety features or patch bugs in existing ones. Design flaws in Uptane can either violate the integrity of the updates to be installed or prevent vehicles from installing new updates, both of which can cause severe safety issues. Previous approaches to protocol verification either fail to capture the necessary features of Uptane or suffer from termination issues due to Uptane’s complexity. A key component of our approach lies in the eager combination of an infinite-state model checker and a cryptographic protocol verifier, where (in contrast to prior lazy approaches) we are able to eliminate a key manual step in the workflow while enabling reasoning over more fine-grained message structures. In addition, our approach utilizes two proven soundness- and completeness-preserving state-space-reduction optimizations for computational tractability, as well as a meta-level analysis technique that makes it feasible to reason over Uptane’s set of optional protocol features. Our approach is able to discover six new vulnerabilities while rediscovering all five known ones. While there have been previous analyses of Uptane’s security properties, they either missed design flaws identified by our approach or suffered from coverage and termination issues. The Uptane standards body has positively acknowledged our findings and has suggested updates to the protocol specification documents to address them.

We present ARMOR, the first substantial effort towards an X.509 certificate chain validation logic (CCVL) implementation with formal, machine-checked correctness guarantees for a large portion of RFC 5280. ARMOR is designed with the twofold goal of providing 1) a formal, machine checked alternative to the RFC specifications, and 2) a reference implementation and test oracle. ARMOR features a modular architecture in which the X.509 CCVL is decomposed into several modules, each of which is independently specified, implemented, and verified. Currently, the formally verified modules of ARMOR include those for the specification and parsing of (subsets of) the PEM and ASN.1 X.690 DER languages, certificate chain building, and many semantic properties concerning required properties of fields within a single certificate and across certificates in a chain. To empirically evaluate its achievement of these goals, we compare ARMOR with 11 open-source X.509 implementations and an open-source certificate linter for its specificational accuracy and runtime overhead. In our evaluation, although ARMOR incurs a high overhead, through its use we are able to detect several noncompliances. Finally, we show an end-to-end application of ARMOR by integrating it with the TLS 1.3 implementation of BoringSSL and testing it with Curl.

Many solutions have been proposed to curb unexpected behavior of automation apps installed on programmable IoT platforms by enforcing safety policies at runtime. However, all prior work addresses a weaker version of the actual problem due to a simpler, unrealistic threat model. These solutions are not general enough as they are heavily dependent on the installed apps and catered to specific IoT platforms. Here, we address a stronger version of the problem via a realistic threat model, where (i) undesired cyber actions can come from not only automation platform backends (e.g., SmartThings) but also close-sourced third-party services (e.g., IFTTT), and (ii) physical actions (e.g., user interactions) on devices can move the IoT system to an undesirable state. We propose a runtime mechanism, dubbed Maverick, which employs an app-independent, platform-agnostic mediator to enforce policies against all undesired cyber actions and applies corrective-actions to bring the IoT system back to a safe state from an unsafe state transition. Maverick is equipped with a policy language capable of expressing rich temporal invariants and an automated toolchain that includes a policy synthesizer and a policy analyzer for user assistance. We implemented Maverick in a prototype and showed its efficacy in both physical and virtual testbeds, incurring minimal overhead.

Cellular networks nowadays are not only responsible for powering up worldwide communication systems, but also enable highly sensitive applications, such as the earthquake and tsunami warning system (ETWS), telemedicine, and autonomous vehicle communication. Due to its importance, one would expect this technology to be highly robust, secure, and reliable. However, even in the newest generations (i.e., 5G), this is not the case. Due to either implementation slipups [6, 11], errors in the standard [3, 5], or misconfigurations [2]. These errors enable numerous destructive attacks, enabling malicious parties to track a victim's location, disrupt cellular services, and eavesdrop on calls, among other implications. To make matters worse, developing defenses against these types of attacks is a non-trivial task as it requires network operator cooperation. Most importantly it requires a significant amount of resources to be allocated by network operators and device manufacturers [2]. To justify allocating resources to fix these issues, network operators need to quantify the misbehaviors and attacks being carried out in the wild. Unfortunately, there is no mechanism in place to perform this type of measurement.

Cryptographic protocols are often expected to be provably secure. However, this security guarantee often falls short in practice due to various implementation flaws. We propose a new paradigm calledcryptographic program analysis (CPA)which prescribes the use of program analysis to detect these implementation flaws at compile time. The principal insight of the CPA is that many of these flaws in cryptographic implementations can be mapped to the violation ofmeta-level propertiesof implementations. A program property that is necessary to realize a cryptographic property is referred to as meta-level property. We show that violations of these meta-level properties can be identified at compile-time that can serve as sufficient evidence of the encompassing flaws. We investigated existing literature on cryptographic implementation flaws and derived 25 corresponding meta-level properties. To instantiate the abstract paradigm of CPA, we develop a specification language based on deterministic finite automaton (DFA) and show that most of the meta-level properties can be expressed in terms of our language. We then develop a tool calledTaintCryptwhich uses static taint analysis to identify meta-level property violations of C/C++ cryptographic implementations at compile-time. We demonstrate the efficacy ofTaintCryptby analyzing open-source C/C++ cryptographic libraries (e.g., OpenSSL) and observe thatTaintCryptcould have helped to avoid several high-profile flaws. We also evaluatedTaintCrypton 5 popular applications and libraries, which generated new security insights. The experimental evaluation on large-scale projects indicates the scalability of our approach.

The X.509 Public-Key Infrastructure (PKI) standard is widely used as a scalable and flexible authentication mechanism. Flaws in X.509 implementations can make relying applications susceptible to impersonation attacks or interoperability issues. In practice, many libraries implementing X.509 have been shown to suffer from flaws that are due to noncompliance with the standard. Developing a compliant implementation is especially hindered by the design complexity, ambiguities, or under-specifications in the standard written in natural languages. In this paper, we set out to alleviate this unsatisfactory state of affairs by re-engineering and formalizing a widely used fragment of the X.509 standard specification, and then using it to develop a high-assurance implementation. Our X.509 specification re-engineering effort is guided by the principle of decoupling the syntactic requirements from the semantic requirements. For formalizing the syntactic requirements of X.509 standard, we observe that a restricted fragment of attribute grammar is sufficient. In contrast, for precisely capturing the semantic requirements imposed on the most-widely used X.509 features, we use quantifier-free first-order logic (QFFOL). Interestingly, using QFFOL results in an executable specification that can be efficiently enforced by an SMT solver. We use these and other insights to develop a high-assurance X.509 implementation named CERES. A comparison of CERES with 3 mainstream libraries (i.e., mbedTLS, OpenSSL, and GnuTLS) based on 2 million real certificate chains and 2 million synthetic certificate chains shows that CERES rightfully rejects malformed and invalid certificates.

In this paper, we perform the first multifaceted measurement study to investigate the widespread insecure practices employed by tertiary education institutes (TEIs) around the globe when offering WPA2-Enterprise Wi-Fi services. The security of such services critically hinges on two aspects: (1) the connection configuration on the client-side; and (2) the TLS setup on the authentication servers. Weaknesses in either can leave users susceptible to credential theft. Typically, TEIs prescribe to their users either manual instructions or pre-configured profiles (e.g., eduroam CAT). For studying the security of configurations, we present a framework in which each configuration is mapped to an abstract security label drawn from a strict partially ordered set. We first used this framework to evaluate the configurations supported by the user interfaces (UIs) of mainstream operating systems (OSs), and discovered many design weaknesses. We then considered 7045 TEIs in 54 countries/regions, and collected 7275 configuration instructions from 2061 TEIs. Our analysis showed that majority of these instructions lead to insecure configurations, and nearly 86% of those TEIs can suffer from credential thefts on at least one OS. We also analyzed a large corpus of pre-configured eduroam CAT profiles and discovered several misconfiguration issues that can negatively impact security. Finally, we evaluated the TLS parameters used by authentication servers of thousands of TEIs and discovered perilous practices, such as the use of expired certificates, deprecated versions of TLS, weak signature algorithms, and suspected cases of private key reuse among TEIs. Our long list of findings have been responsibly disclosed to the relevant stakeholders, many of which have already been positively acknowledged.

The paper focuses on developing an automated black-box testing approach called DIKEUE that checks 4G Long Term Evolution (LTE) control-plane protocol implementations in commercial-off-the-shelf (COTS) cellular devices (also, User Equipments or UEs) for noncompliance with the standard. Unlike prior noncompliance checking approaches which rely on property-guided testing, DIKEUE adopts a property-agnostic, differential testing approach, which leverages the existence of many different control-plane protocol implementations in COTS UEs. DIKEUE uses deviant behavior observed during differential analysis of pairwise COTS UEs as a proxy for identifying noncompliance instances. For deviant behavior identification, DIKEUE first uses black-box automata learning, specialized for 4G LTE control-plane protocols, to extract input-output finite state machine (FSM) for a given UE. It then reduces the identification of deviant behavior in two extracted FSMs as a model checking problem. We applied DIKEUE in checking noncompliance in 14 COTS UEs from 5 vendors and identified 15 new deviant behavior as well as 2 previous implementation issues. Among them, 11 are exploitable whereas 3 can cause potential interoperability issues.

This paper focuses on developing an automatic, black-box testing approach called Morpheus to check the non-compliance of libraries implementing PKCS#1-v1.5 signature verification with the PKCS#1-v1.5 standard. Non-compliance can not only make implementations vulnerable to Bleichenbacher-style RSA signature forgery attacks but also can induce interoperability issues. For checking non-compliance, Morpheus adaptively generates interesting test cases and then takes advantage of an oracle, a formally proven correct implementation of PKCS#1-v1.5 signature standard, to detect non-compliance in an implementation under test. We have used Morpheus to test 45 implementations of PKCS#1-v1.5 signature verification and discovered that 6 of them are susceptible to variants of the Bleichenbacher-style low public exponent RSA signature forgery attack, 1 implementation has a buffer overflow, 33 implementations have incompatibility issues, and 8 implementations have minor leniencies. Our findings have been responsibly disclosed and positively acknowledged by the developers.

We present an efficient approach to learn past-time linear temporal logic formulas (PLTL) from a set of propositional variables and a sample of finite traces over those variables.The efficiency of our approach can be attributed to a careful encoding of the PLTL formula learning problem as a bit-vector function synthesis problem, and the use of an enhanced Syntax-Guided Synthesis (SyGuS) engine to solve the latter.We implemented our approach in a tool called SYSLITE and empirically evaluated its efficacy with two case studies.In these case studies, we observe that SYSLITE on average enjoys a speedup of 44x over current learning approaches for temporal formulas while learning the expected formulas in the vast majority of cases.

Abstract This paper focuses on protecting the cellular paging protocol — which balances between the quality-of-service and battery consumption of a device — against security and privacy attacks. Attacks against this protocol can have severe repercussions, for instance, allowing attacker to infer a victim’s location, leak a victim’s IMSI, and inject fabricated emergency alerts. To secure the protocol, we first identify the underlying design weaknesses enabling such attacks and then propose efficient and backward-compatible approaches to address these weaknesses. We also demonstrate the deployment feasibility of our enhanced paging protocol by implementing it on an open-source cellular protocol library and commodity hardware. Our evaluation demonstrates that the enhanced protocol can thwart attacks without incurring substantial overhead.

This paper focuses on checking the correctness and robustness of the AT command interface exposed by the cellular baseband processor through Bluetooth and USB. A device's application processor uses this interface for issuing high-level commands (or, AT commands) to the baseband processor for performing cellular network operations (e.g., placing a phone call). Vulnerabilities in this interface can be leveraged by malicious Bluetooth peripherals to launch pernicious attacks including DoS and privacy attacks. To identify such vulnerabilities, we propose ATFuzzer that uses a grammar-guided evolutionary fuzzing approach which mutates production rules of the AT command grammar instead of concrete AT commands. Empirical evaluation with ATFuzzer on 10 Android smartphones from 6 vendors revealed 4 invalid AT command grammars over Bluetooth and 13 over USB with implications ranging from DoS, downgrade of cellular protocol version (e.g., from 4G to 3G/2G) to severe privacy leaks. The vulnerabilities along with the invalid AT command grammars were responsibly disclosed to affected vendors and two of the reported vulnerabilities have been already assigned CVEs (CVE-2019-16400 and CVE-2019-16401).

The paper proposes 5GReasoner, a framework for property-guided formal verification of control-plane protocols spanning across multiple layers of the 5G protocol stack. The underlying analysis carried out by 5GReasoner can be viewed as an instance of the model checking problem with respect to an adversarial environment. Due to an effective use of behavior-specific abstraction in our manually extracted 5G protocol, 5GReasoner's analysis generalizes prior analyses of cellular protocols by reasoning about properties not only regarding packet payload but also multi-layer protocol interactions. We instantiated 5GReasoner with two model checkers and a cryptographic protocol verifier, lazily combining them through the use of abstraction-refinement principle. Our analysis of the extracted 5G protocol model covering 6 key control-layer protocols spanning across two layers of the 5G protocol stack with 5GReasoner has identified 11 design weaknesses resulting in attacks having both security and privacy implications. Our analysis also discovered 5 previous design weaknesses that 5G inherits from 4G, and can be exploited to violate its security and privacy guarantees.

This paper focuses on developing a security mechanism geared towards appified smart-home platforms. Such platforms often expose programming interfaces for developing automation apps that mechanize different tasks among smart sensors and actuators (e.g., automatically turning on the AC when the room temperature is above 80 F). Due to the lack of effective access control mechanisms, these automation apps can not only have unrestricted access to the user's sensitive information (e.g., the user is not at home) but also violate user expectations by performing undesired actions. As users often obtain these apps from unvetted sources, a malicious app can wreak havoc on a smart-home system by either violating the user's security and privacy, or creating safety hazards (e.g., turning on the oven when no one is at home). To mitigate such threats, we propose Expat which ensures that user expectations are never violated by the installed automation apps at runtime. To achieve this goal, Expat provides a platform-agnostic, formal specification language UEI for capturing user expectations of the installed automation apps' behavior. For effective authoring of these expectations (as policies) in UEI, Expat also allows a user to check the desired properties (e.g., consistency, entailment) of them; which due to their formal semantics can be easily discharged by an SMT solver. Expat then enforces UEI policies in situ with an inline reference monitor which can be realized using the same app programming interface exposed by the underlying platform. We instantiate Expat for one of the representative platforms, OpenHAB, and demonstrate it can effectively mitigate a wide array of threats by enforcing user expectations while incurring only modest performance overhead.

In the cellular ecosystem, base stations act as trusted intermediaries between cellular devices and the core network. During connection bootstrapping, devices currently, however, do not possess any mechanisms to authenticate a base station before connecting to it. This lack of authentication has been shown to be exploitable by adversaries to install fake base stations which can lure unsuspecting devices to connect to them and then launch sophisticated attacks. Despite being a well-known threat to the cellular ecosystem, this weakness is not addressed in the current protocol versions including 5G. The current paper sets out to fill this void by proposing a Public-key infrastructure (PKI) based authentication mechanism which builds on top of the asymmetric cryptography used in 5G and adheres to the relevant deployment constraints. Our proposed authentication scheme leverages precomputation-based digital signature generation algorithms and employs optimizations in three dimensions---PKI scheme-level, protocol-level, and cryptographic scheme-level---to address the trilemma of small signature size, efficient signature generation, and short verification time. Our evaluation on a real testbed indicates that the proposed scheme is not only readily deployable but also performs better than a symmetric key-based scheme (i.e., TESLA) in terms of security guarantee, overhead, and deployment constraints (e.g., backward compatibility).

Mobile devices are becoming the default platform for multimedia content consumption. Such a thriving business ecosystem has drawn interests from content distributors to develop apps that can reach a large number of audience. The business-edge of content delivery apps crucially relies on being able to effectively arbitrate the purchase and delivery of contents, and govern the access of contents with respect to usage control policies, on a plethora of consumer devices. Content protection on mobile platforms, especially in the absence of Trusted Execution Environment (TEE), is a challenging endeavor where developers often have to resort to ad-hoc deterrence-based defenses. This work evaluates the effectiveness of content protection mechanisms embraced by vendors of content delivery apps, with respect to a hierarchy of adversaries with varying real-world capabilities. Our analysis of 141 vulnerable apps uncovered that, in many cases, due to developers' unjustified trust assumptions about the underlying technologies, adversaries can obtain unauthorized and unrestricted access to contents of apps, sometimes without even needing to reverse engineer the deterrence-based defenses. Some weaknesses in the apps can also severely impact app users' security and privacy. All our findings have been responsibly disclosed to the corresponding app vendors.

Developing a secure system (or, protocol) in general boils down to having a correct and robust specification which developers faithfully implement with the available platform support. Vulnerabilities can thus crop up due to inadequate specification, buggy implementations, or the lack of appropriate security constructs in the platform. In this talk, I will present examples of insecurity due to inadequate specification, wrong implementations, and deficient platform support. I will particularly focus on how automated reasoning and formal verification techniques can greatly contribute towards detecting vulnerabilities. In the first example, I will show how 4G LTE telecommunication protocol specification lacks security considerations which can be exploited by adversaries to have catastrophic impacts. Next, I will present how incorrect X.509 certificate validation implementations in open-source SSL/TLS libraries leave users prone to impersonation attacks. Finally, I will conclude my talk with a discussion of how lack of hardware support makes enforcing Digital Rights Management (DRM) policies infeasible for mobile devices.

Network protocol implementations must comply with their specifications that include properties describing the correct operational behavior of the protocol in response to different temporal orderings of network events. Due to inconsistent interpretations of the specification, developers can unknowingly introduce semantic bugs, which cause the implementations to violate the respective properties. Detecting such bugs in stateful protocols becomes significantly difficult as their operations depend on their internal state machines and the complex interactions between the protocol logic. In this paper, we present an automated tool to help developers analyze their protocol implementations and detect semantic bugs violating the temporal properties of the protocols. Given an implementation, our tool (1) extracts the implemented finite state machine (FSM) of the protocol from the source code by symbolically exploring the code and (2) determines whether the extracted FSM violates given temporal properties by using an off-the-shelf model checker. We demonstrated the efficacy of our tool by applying it on 6 protocol implementations. We detected 11 semantic bugs (2 with security implications) when we analyzed these implementations against properties obtained from their publicly available specifications.

The X.509 Public-Key Infrastructure has long been used in the SSL/TLS protocol to achieve authentication. A recent trend of Internet-of-Things (IoT) systems employing small footprint SSL/TLS libraries for secure communication has further propelled its prominence. The security guarantees provided by X.509 hinge on the assumption that the underlying implementation rigorously scrutinizes X.509 certificate chains, and accepts only the valid ones. Noncompliant implementations of X.509 can potentially lead to attacks and/or interoperability issues. In the literature, black-box fuzzing has been used to find flaws in X.509 validation implementations, fuzzing, however, cannot guarantee coverage and thus severe flaws may remain undetected. To thoroughly analyze X.509 implementations in small footprint SSL/TLS libraries, this paper takes the complementary approach of using symbolic execution. We observe that symbolic execution, a technique proven to be effective in finding software implementation flaws, can also be leveraged to expose noncompliance in X.509 implementations. Directly applying an off-the-shelf symbolic execution engine on SSL/TLS libraries is, however, not practical due to the problem of path explosion. To this end, we propose the use of SymCerts, which are X.509 certificate chains carefully constructed with a mixture of symbolic and concrete values. Utilizing SymCerts and some domain-specific optimizations, we symbolically execute the certificate chain validation code of each library and extract path constraints describing its accepting and rejecting certificate universes. These path constraints help us identify missing checks in different libraries. For exposing subtle but intricate noncompliance with X.509 standard, we cross-validate the constraints extracted from different libraries to find further implementation flaws. Our analysis of 9 small footprint X.509 implementations has uncovered 48 instances of noncompliance. Findings and suggestions provided by us have already been incorporated by developers into newer versions of their libraries.

Visual cryptography has been applied to design human computable authentication protocols. In such a protocol, the user and the server share a secret key in the form of an image printed on a transparent medium, which the user superimposes on server-generated image challenges, and visually decodes a response code from the image. An example of such protocols is PassWindow, an award-winning commercial product. We study the security and usability of segment-based visual cryptographic authentication protocols (SVAPs), which include PassWindow as a special case. In SVAP, the images consist of segments and are thus structured. Our overall findings are negative. We introduce two attacks that together are able to break all SVAPs we considered in the paper. Furthermore, our attacks exploit fundamental weaknesses of SVAPs that appear difficult to fix. We have also evaluated the usability of different SVAPs, and found that the protocol that offers the best security has the poorest usability.

Mnemonic strategy has been recommended to help users generate secure and memorable passwords. We evaluated the security of $6$ mnemonic strategy variants in a series of online studies involving $5,484$ participants. In addition to applying the standard method of using guess numbers or similar metrics to compare the generated passwords, we also measured the frequencies of the most commonly chosen sentences as well as the resulting passwords. While metrics similar to guess numbers suggested that all variants provided highly secure passwords, statistical metrics told a different story. In particular, differences in the exact instructions had a tremendous impact on the security level of the resulting passwords. We examined the mental workload and memorability of 2 mnemonic strategy variants in another online study with $752$ participants. Although perceived workloads for the mnemonic strategy variants were higher than that for the control group where no strategy is required, no significant reduction in password recall after $1$ week was obtained.

Firewall policies are notorious for having misconfiguration errors which can defeat its intended purpose of protecting hosts in the network from malicious users. We believe this is because today's firewall policies are mostly monolithic. Inspired by ideas from modular programming and code refactoring, in this work we introduce three kinds of modules: primary, auxiliary, and template, which facilitate the refactoring of a firewall policy into smaller, reusable, comprehensible, and more manageable components. We present algorithms for generating each of the three modules for a given legacy firewall policy. We also develop ModFP, an automated tool for converting legacy firewall policies represented in access control list to their modularized format. With the help of ModFP, when examining several real-world policies with sizes ranging from dozens to hundreds of rules, we were able to identify subtle errors.

To reduce costs, organizations may outsource data storage and data processing to third-party clouds. This raises confidentiality concerns, since the outsourced data may have sensitive information. Although semantically secure encryption of the data prior to outsourcing alleviates these concerns, it also renders the outsourced data useless for any relational processing. Motivated by this problem, we present two database encryption schemes that reveal just enough information about structured data to support a wide-range of relational queries. Our main contribution is a definition and proof of security for the two schemes. This definition captures confidentiality offered by the schemes using a novel notion of equivalence of databases from the adversary's perspective. As a specific application, we adapt an existing algorithm for finding violations of a rich class of privacy policies to run on logs encrypted under our schemes and observe low to moderate overheads.

Organizations collect personal information from individuals to carry out their business functions. Federal privacy regulations, such as the Health Insurance Portability and Accountability Act (HIPAA), mandate how this collected information can be shared by the organizations. It is thus incumbent upon the organizations to have means to check compliance with the applicable regulations. Prior work by Barth et. al. introduces two notions of compliance, weak compliance (WC) and strong compliance (SC). WC ensures that present requirements of the policy can be met whereas SC also ensures obligations can be met. An action is compliant with a privacy policy if it is both weakly and strongly compliant. However, their definitions of compliance are restricted to only propositional linear temporal logic (pLTL), which cannot feasibly specify HIPAA. To this end, we present a policy specification language based on a restricted subset of first order temporal logic (FOTL) which can capture the privacy requirements of HIPAA. We then formally specify WC and SC for policies of our form. We prove that checking WC is feasible whereas checking SC is undecidable. We then formally specify the property WC entails SC, denoted by Δ, which requires that each weakly compliant action is also strongly compliant. To check whether an action is compliant with such a policy, it is sufficient to only check whether the action is weakly compliant with that policy. We also prove that when a policy ℘ has the Δ-property, the present requirements of the policy reduce to the safety requirements imposed by ℘. We then develop a sound, semi-automated technique for checking whether practical policies have the Δ-property. We finally use HIPAA as a case study to demonstrate the efficacy of our policy analysis technique.

In the current time of the Internet, specifically with the emergence of social networking, people are sharing both sensitive and non-sensitive information among each other without understanding its consequences. Federal regulations exist to mandate how sensitive information (e.g., SSN, health records, etc.) of a person can be shared (or, used) by organizations. However, there are no established norms or practices regarding how information that is deemed to be not sensitive may be used or shared. Furthermore, for the sake of transparency, different organizations reveal small amounts of non-sensitive information (i.e., photos, salaries, work hours, size of the houses, etc.) about their clients or employees. Although such information seems insignificant, the aggregation of it can be used to create a partial profile of a person which can later be used by malicious parties for robbery, extortion, kidnapping, etc. The goal of this work is to create awareness by demonstrating that it is plausible to create such a partial profile of a person just by crawling the Internet. For this, we have developed an open source framework that generates batch crawlers to create partial profiles of individuals. We also show empirical comparisons of the amount of information that can be gathered by using free and also paid websites.

User obligations are actions that the human users are required to perform in some future time. These are common in many practical access control and privacy and can depend on and affect the authorization state. Consequently, a user can incur an obligation that she is not authorized to perform which may hamper the usability of a system. To mitigate this problem, previous work introduced a property of the authorization state, accountability, which requires that all the obligatory actions to be authorized when they are attempted. Although, existing work provides a specific and tractable decision procedure for a variation of the accountability property, it makes a simplified assumption that no cascading obligations may happen, i.e., obligatory actions cannot further incur obligations. This is a strong assumption which reduces the expressive power of past models, and thus cannot support many obligation scenarios in practical security and privacy policies. In this work, we precisely specify the strong accountability property in the presence of cascading obligations and prove that deciding it is NP-hard. We provide for several special yet practical cases of cascading obligations (i.e., repetitive, finite cascading, etc.) a tractable decision procedure for accountability. Our experimental results illustrate that supporting such special cases is feasible in practice.

This paper is part of a project investigating authorization systems that assign obligations to users. We are particularly interested in obligations that require authorization to be performed and that, when performed, may modify the authorization state. In this context, a user may incur an obligation she is unauthorized to perform. Prior work has introduced a property of the authorization system state that ensures users will be authorized to fulfill their obligations. We call this property accountability because users that fail to perform authorized obligations are accountable for their non-performance. While a reference monitor can mitigate violations of accountability, it cannot prevent them entirely. This paper presents techniques to be used by obligation system managers to restore accountability. We introduce several notions of dependence among pending obligations that must be considered in this process. We also introduce a novel notion we call obligation pool slicing, owing to its similarity to program slicing. An obligation pool slice identifies a set of obligations that the administrator may need to consider when applying strategies proposed here for restoring accountability. The paper also presents the system architecture of an authorization system that incorporates obligations that can require and affect authorizations.

Many authorization system models include some notion of obligation. Little attention has been given to user obligations that depend on and affect authorizations. However, to be usable, the system must ensure users have the authorizations they need when their obligations must be performed. Prior work in this area introduced accountability properties that ensure failure to fulfill obligations is not due to lack of required authorizations. That work presented inconclusive and purely theoretical results concerning the feasibility of maintaining accountability in practice. The results of the current paper include algorithms and performance analysis that support the thesis that maintaining accountability in a reference monitor is reasonable in many applications.