In this paper, we revisit the problem of TLS version downgrade, with a specific focus on enterprise software, which are applications that play direct roles in the daily operations of an organization, including remote desktop, email, and VPN clients. Although TLS version downgrade is a classic problem, previous studies have mostly focused on its manifestations in browser applications. However, as TLS continues to gain prominence in other application scenarios, it is crucial to also investigate the implementation and deployment of TLS in other mission-critical appliances that depend upon TLS for their corresponding security guarantees. To this end, we identified and tested 217 enterprise software on 4 mainstream operating systems (OSes) for how they implement and deploy TLS downgrade defenses. We carefully designed a series of experiments to determine whether a client-side enterprise software is vulnerable to downgrade attacks. Results of our experiments paint the enterprise software ecosystem in a positive light, as only 8 enterprise client applications exhibit some vulnerabilities to TLS version downgrade due to missing protection mechanisms. Given the availability and low costs of standardized downgrade defenses, we champion their adoption by software vendors to put an end to the threat of TLS version downgrade. Finally, as various industries are moving away from legacy versions of TLS, it is also time for enterprise software vendors to rethink the necessity and merits of supporting old TLS versions in their products.

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.

In the context of connecting to enterprise Wi-Fi, previous works show that relying on human users to manually configure or enforce server authentication often leads to insecure outcomes. Consequently, many user credentials can potentially be stolen by the so-called "Evil-Twin'' (ET) attack. To ease the burden of human users, various easy-to-use Wi-Fi configurators have been released and deployed. In this work, we investigate whether such configurators can indeed protect users from variants of the ET attack. To our surprise, the results of our investigation show that all configurators considered in the study suffer from certain weaknesses due to their design, implementation, or deployment practices. Notable findings include a series of design flaws in the new trust-on-first-use (TOFU) configurator on Android (available since version 12), which can be exploited in tandem to achieve a stealthy ET attack. Moreover, we found that 2 open-source Android Wi-Fi configurators fail to properly enforce server authentication under specific situations. The cause of these could be partly attributed to the complexity stemmed from certificate name matching as well as the limitations of the Android API. Last but not least, we found that a commercial configurator not only allows insecure Wi-Fi configurations to be deployed, but also the covert injection of certificates on the user device to facilitate interception of other TLS traffic, posing yet another hidden security and privacy threat to its users. All in all, this study shows that despite years of research on the topic, developing a user-friendly yet reliable Wi-Fi configurator remains an elusive goal, and thus the threat of ET attacks continues to be relevant. As such, it is time to rethink whether the complexity of the standard certificate chain validation is actually good for enterprise Wi-Fi.

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.

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.

Image classifiers often suffer from adversarial examples, which are generated by strategically adding a small amount of noise to input images to trick classifiers into misclassification. Over the years, many defense mechanisms have been proposed, and different researchers have made seemingly contradictory claims on their effectiveness. We present an analysis of possible adversarial models, and propose an evaluation framework for comparing different defense mechanisms. As part of the framework, we introduce a more powerful and realistic adversary strategy. Furthermore, we propose a new defense mechanism called Random Spiking (RS), which generalizes dropout and introduces random noises in the training process in a controlled manner. Evaluations under our proposed framework suggest RS delivers better protection against adversarial examples than many existing schemes.

Despite years of research, many existing e-voting systems do not adequately protect voting privacy. In most cases, such systems only achieve "immediate privacy", that is, they only protect voting privacy against today's adversaries, but not against a future adversary, who may possess better attack technologies like new cryptanalysis algorithms and/or quantum computers. Previous attempts at providing long-term voting privacy (dubbed "everlasting privacy" in the literature) often require additional trusts in parties that do not need to be trusted for immediate privacy.

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.

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.