An official website of the United States government
We present a principled automatic testing framework for application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined within the Coq interactive theorem prover, supporting a smooth transition from testing to formal verification. Given a server model, we show how to automatically derive a tester that probes the server for unexpected behaviors. We address the uncertainties caused by both the server's internal choices and the network delaying messages nondeterministically. The derived tester accepts server implementations whose possible behaviors are a subset of those allowed by the nondeterministic model. We demonstrate the effectiveness of this framework by using it to specify and test a fragment of the HTTP protocol, showing that the automatically derived tester can capture RFC violations in buggy server implementations, including the latest versions of Apache and Nginx.
more »
« less
Practical and Scalable Security Verification of Secure Architectures
We present a new and practical framework for security verification of secure architectures. Specifically, we break the verification task into external verification and internal verification. External verification considers the external protocols, i.e. interactions between users, compute servers, network entities, etc. Meanwhile, internal verification considers the interactions between hardware and software components within each server. This verification framework is general-purpose and can be applied to a stand-alone server, or a large-scale distributed system. We evaluate our verification method on the CloudMonatt and HyperWall architectures as examples.
more »
« less
- Award ID(s):
- 1814190
- PAR ID:
- 10392215
- Date Published:
- Journal Name:
- Hardware and Architectural Support for Security and Privacy
- Page Range / eLocation ID:
- 1 to 9
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Connected vehicles (CVs) have facilitated the development of intelligent transportation system that supports critical safety information sharing with minimum latency. However, CVs are vulnerable to different external and internal attacks. Though cryptographic techniques can mitigate external attacks, preventing internal attacks imposes challenges due to authorized but malicious entities. Thwarting internal attacks require identifying the trustworthiness of the participating vehicles. This paper proposes a trust management framework for CVs using interaction provenance that ensures privacy, considers both in-vehicle and vehicular network security incidents, and supports flexible security policies. For this purpose, we present an interaction provenance recording and trust management protocol. Different events are extracted from interaction provenance, and trustworthiness is calculated using fuzzy policies based on the events.more » « less
-
We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.more » « less
-
Connected autonomous vehicles (CAVs) have fostered the development of intelligent transportation systems that support critical safety information sharing with minimum latency and making driving decisions autonomously. However, the CAV environment is vulnerable to different external and internal attacks. Authorized but malicious entities which provide wrong information impose challenges in preventing internal attacks. An essential requirement for thwarting internal attacks is to identify the trustworthiness of the vehicles. This paper exploits interaction provenance to propose a trust management framework for CAVs that considers both in-vehicle and vehicular network security incidents, supports flexible security policies and ensures privacy. The framework contains an interaction provenance recording and trust management protocol that extracts events from interaction provenance and calculates trustworthiness using fuzzy policies based on the events. Simulation results show that the framework is effective and can be integrated with the CAV stack with minimal computation and communication overhead.more » « less
-
ABSTRACT We develop machine learning models that incorporate both external (deterministic) and internal (voluntaristic) factors affecting firm failure and survival. Using structured and unstructured data, we empirically investigate the external and internal factors that affect the US manufacturing firms’ business failure. We also examine how the interactions between external shocks and firm responses impact business failure. Our findings indicate that while external factors can significantly impact the likelihood that firms fail, specific management responses to these challenges can effectively mitigate the negative effects and contribute to firm survival.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3505253.3505256
