Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Formal TLS Handshake Model in LNT
71
0
0.0
(
0
)
Added by
EPTCS
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Josip Bozic
Ask ChatGPT about the research
No Arabic abstract
Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.
rate research
Read More
Network middle-boxes often classify the traffic flows on the Internet to perform traffic management or discriminate one traffic against the other. As the widespread adoption of HTTPS protocol has made it difficult to classify the traffic looking into the content field, one of the fields the middle-boxes look for is Server Name Indicator (SNI), which goes in plain text. SNI field contains information about the host and can, in turn, reveal the type of traffic. This paper presents a method to mask the server host identity by encrypting the SNI. We develop a simple method that completes the SSL/TLS connection establishment over two handshakes - the first handshake establishes a secure channel without sharing SNI information, and the second handshake shares the encrypted SNI. Our method makes it mandatory for fronting servers to always accept the handshake request without the SNI and respond with a valid SSL certificate. As there is no modification in already proven SSL/TLS encryption mechanism and processing of handshake messages, the new method enjoys all security benefits of existing secure channel establishment and needs no modification in existing routers/middle-boxes. Using customized client-server over the live Internet, we demonstrate the feasibility of our method. Moreover, the impact analysis shows that the method adheres to almost all SSL/TLS related Internet standards requirements.
The rowhammer bug allows an attacker to gain privilege escalation or steal private data. A key requirement of all existing rowhammer attacks is that an attacker must have access to at least part of an exploitable hammer row. We refer to such rowhammer attacks as PeriHammer. The state-of-the-art software-only defenses against PeriHammer attacks is to make the exploitable hammer rows beyond the attackers access permission. In this paper, we question the necessity of the above requirement and propose a new class of rowhammer attacks, termed as TeleHammer. It is a paradigm shift in rowhammer attacks since it crosses privilege boundary to stealthily rowhammer an inaccessible row by implicit DRAM accesses. Such accesses are achieved by abusing inherent features of modern hardware and or software. We propose a generic model to rigorously formalize the necessary conditions to initiate TeleHammer and PeriHammer, respectively. Compared to PeriHammer, TeleHammer can defeat the advanced software-only defenses, stealthy in hiding itself and hard to be mitigated. To demonstrate the practicality of TeleHammer and its advantages, we have created a TeleHammers instance, called PThammer, which leverages the address-translation feature of modern processors. We observe that a memory access from user space can induce a load of a Level-1 page-table entry (L1PTE) from memory and thus hammer the L1PTE once, although L1PTE is not accessible to us. To achieve a high enough hammering frequency, we flush relevant TLB and cache effectively and efficiently. To this end, we demonstrate PThammer on three different test machines and show that it can cross user-kernel boundary and induce the first bit flips in L1PTEs within 15 minutes of double-sided PThammering. We have exploited PThammer to defeat advanced software-only rowhammer defenses in default system setting.
The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches.
Software defined networking (SDN) has been adopted to enforce the security of large-scale and complex networks because of its programmable, abstract, centralized intelligent control and global and real-time traffic view. However, the current SDN-based security enforcement mechanisms require network managers to fully understand the underlying configurations of network. Facing the increasingly complex and huge SDN networks, we urgently need a novel security policy management mechanism which can be completely transparent to any underlying information. That is it can permit network managers to define upper-level security policies without containing any underlying information of network, and by means of model transformation system, these upper-level security policies can be transformed into their corresponding lower-level policies containing underlying information automatically. Moreover, it should ensure system model updated by the generated lower-level policies can hold all of security properties defined in upper-level policies. Based on these insights, we propose a security policy model transformation and verification approach for SDN in this paper. We first present the formal definition of a security policy model (SPM) which can be used to specify the security policies used in SDN. Then, we propose a model transformation system based on SDN system model and mapping rules, which can enable network managers to convert SPM model into corresponding underlying network configuration policies automatically, i.e., flow table model (FTM). In order to verify SDN system model updated by the generated FTM models can hold the security properties defined in SPM models, we design a security policy verification system based on model checking. Finally, we utilize a comprehensive case to illustrate the feasibility of the proposed approach.
Googles CECPQ1 experiment in 2016 integrated a post-quantum key-exchange algorithm, newhope1024, into TLS 1.2. The Google-Cloudflare CECPQ2 experiment in 2019 integrated a more efficient key-exchange algorithm, ntruhrss701, into TLS 1.3. This paper revisits the choices made in CECPQ2, and shows how to achieve higher performance for post-quantum key exchange in TLS 1.3 using a higher-security algorithm, sntrup761. Previous work had indicated that ntruhrss701 key generation was much faster than sntrup761 key generation, but this paper makes sntrup761 key generation much faster by generating a batch of keys at once. Batch key generation is invisible at the TLS protocol layer, but raises software-engineering questions regarding the difficulty of integrating batch key exchange into existing TLS libraries and applications. This paper shows that careful choices of software layers make it easy to integrate fast post-quantum software, including batch key exchange, into TLS with minor changes to TLS libraries and no changes to applications. As a demonstration of feasibility, this paper reports successful integration of its fast sntrup761 library, via a lightly patched OpenSSL, into an unmodified web browser and an unmodified TLS terminator. This paper also reports TLS 1.3 handshake benchmarks, achieving more TLS 1.3 handshakes per second than any software included in OpenSSL.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
