scholarly journals Experience of Implementation of the Protocol TLS 1.3 Verification

2021 ◽  
Vol 24 (5) ◽  
pp. 902-922
Author(s):  
Алексей Вячеславович Никешин ◽  
Виктор Зиновьевич Шнитман
Keyword(s):  
Cryptographic Protocol ◽  
Formal Specifications ◽  
Exchange Flow ◽  
Testing Methods ◽  
Test Scenario ◽  
System Under Test ◽  
Secure Data Transmission ◽  
Implementation Under Test ◽  
Finite State ◽  
Pass Through

This paper presents the experience of verifying server implementations of the TLS cryptographic protocol version 1.3. TLS is a widely used cryptographic protocol designed to create secure data transmission channels and provides the necessary functionality for this: confidentiality of the transmitted data, data integrity, and authentication of the parties. The new version 1.3 of the TLS protocol was introduced in August 2018 and has a number of significant differences compared to the previous version 1.2. A number of TLS developers have already included support for the latest version in their implementations. These circumstances make it relevant to do research in the field of verification and security of the new TLS protocol implementations. We used a new test suite for verifying implementations of the TLS 1.3 for compliance with Internet specifications, developed on the basis of the RFC8446, using UniTESK technology and mutation testing methods. The current work is part of the TLS 1.3 protocol verification project and covers some of the additional functionality and optional protocol extensions. To test implementations for compliance with formal specifications, UniTESK technology is used, which provides testing automation tools based on the use of finite state machines. The states of the system under test define the states of the state machine, and the test effects are the transitions of this machine. When performing a transition, the specified impact is passed to the implementation under test, after which the implementation's reactions are recorded and a verdict is automatically made on the compliance of the observed behavior with the specification. Mutational testing methods are used to detect non-standard behavior of the system under test by transmitting incorrect data. Some changes are made to the protocol exchange flow created in accordance with the specification: either the values of the message fields formed on the basis of the developed protocol model are changed, or the order of messages in the exchange flow is changed. The protocol model allows one to make changes to the data flow at any stage of the network exchange, which allows the test scenario to pass through all the significant states of the protocol and in each such state to test the implementation in accordance with the specified program. So far, several implementations have been found to deviate from the specification. The presented approach has proven effective in several of our projects when testing network protocols, providing detection of various deviations from the specification and other errors.

scholarly journals Verification of security properties of the TLS 1.3 extensions

2021 ◽  
Author(s):  
Alexei Viacheslavovich Nikeshin ◽  
Victor Zinovievich Shnitman
Keyword(s):  
Cryptographic Protocol ◽  
Formal Specifications ◽  
Exchange Flow ◽  
Testing Methods ◽  
Test Scenario ◽  
System Under Test ◽  
Secure Data Transmission ◽  
Implementation Under Test ◽  
Finite State ◽  
Pass Through

This paper presents the experience of verifying server implementations of the TLS cryptographic protocol version 1.3. TLS is a widely used cryptographic protocol designed to create secure data transmission channels and provides the necessary functionality for this: confidentiality of the transmitted data, data integrity, and authentication of the parties. The new version 1.3 of the TLS protocol was introduced in August 2018 and has a number of significant differences compared to the previous version 1.2. A number of TLS developers have already included support for the latest version in their implementations. These circumstances make it relevant to do research in the field of verification and security of the new TLS protocol implementations. We used a new test suite for verifying implementations of the TLS 1.3 for compliance with Internet specifications, developed on the basis of the RFC8446, using UniTESK technology and mutation testing methods. The current work is part of the TLS 1.3 protocol verification project and covers some of the additional functionality and optional protocol extensions. To test implementations for compliance with formal specifications, UniTESK technology is used, which provides testing automation tools based on the use of finite state machines. The states of the system under test define the states of the state machine, and the test effects are the transitions of this machine. When performing a transition, the specified impact is passed to the implementation under test, after which the implementation's reactions are recorded and a verdict is automatically made on the compliance of the observed behavior with the specification. Mutational testing methods are used to detect non-standard behavior of the system under test by transmitting incorrect data. Some changes are made to the protocol exchange flow created in accordance with the specification: either the values of the message fields formed on the basis of the developed protocol model are changed, or the order of messages in the exchange flow is changed. The protocol model allows one to make changes to the data flow at any stage of the network exchange, which allows the test scenario to pass through all the significant states of the protocol and in each such state to test the implementation in accordance with the specified program. So far, several implementations have been found to deviate from the specification. The presented approach has proven effective in several of our projects when testing network protocols, providing detection of various deviations from the specification and other errors.

Analysis and Testing of Passenger Vehicle Bulkhead Fireworthiness

2017 ◽  
Author(s):  
Brian Herbst ◽  
Steven Meyer ◽  
Lauren Bell ◽  
Jack Bish ◽  
Christopher Clarke
Keyword(s):  
Passenger Vehicle ◽  
Testing Methods ◽  
Fire Propagation ◽  
Testing Methodology ◽  
Seal Design ◽  
Retention Testing ◽  
The Subject ◽  
Occupant Injuries ◽  
Pass Through

This paper presents a case study of an injury producing post-crash fire as well as testing methods to evaluate bulkhead pass through seal fire resistance and retention. In the subject crash, engine compartment fluids were released and ignited. The burning fluids entered the occupant compartment through a bulkhead pass through, resulting in rapid fire propagation and severe occupant injuries before extrication could be completed. A burn testing methodology was developed and used to evaluate the ability of the subject seal design to prevent flames and fluids from entering the occupant compartment. A retention testing methodology was also developed and used to evaluate a variety of seal designs.

scholarly journals Effectiveness of the Reverse Bending and Straightening Tests in Detecting Laminations in Wires for Civil Engineering Applications

2013 ◽  
Vol 59 (4) ◽  
pp. 423-439 ◽  
Author(s):  
K.K. Adewole ◽  
S.J. Bull
Keyword(s):  
Civil Engineering ◽  
Non Destructive Testing ◽  
Testing Methods ◽  
Destructive Testing ◽  
Engineering Applications ◽  
Near Surface ◽  
Fe Simulations ◽  
Pass Through ◽  
Non Destructive

Abstract The reverse bending and straightening test is conducted on wires used for civil engineering applications to detect laminations which can pose a threat to the integrity of the wires. The FE simulations of the reverse bending and straightening of wires with laminations revealed that the reverse bending and straightening test is only effective in revealing or detecting near-surface laminations with lengths from 25mm located up to 30% of the wire’s thickness and may not be an effective test to detect mid-thickness, near-mid-thickness, and short near-surface laminations with lengths below 15mm. This is because wires with mid-thickness, near-mid-thickness and short nearsurface laminations will pass through the reverse bending and straightening procedures without fracturing and therefore mid-thickness, near-mid-thickness and short near-surface laminations may go undetected. Consequently, other in-line non destructive testing methods might have to be used to detect mid-thickness, near-mid-thickness and short near-surface laminations in the wires.

TEST SCENARIO GENERATION BASED ON FORMAL SPECIFICATION AND USAGE PROFILE

2000 ◽  
Vol 10 (02) ◽  
pp. 185-201 ◽  
Author(s):  
KAI H. CHANG ◽  
SHIH-SUNG LIAO ◽  
RICHARD CHAPMAN ◽  
CHUN-YU CHEN
Keyword(s):  
Formal Specification ◽  
State Transition ◽  
Object Oriented ◽  
The State ◽  
State Model ◽  
Scenario Generation ◽  
Formal Specifications ◽  
Test Scenario ◽  
Transition Diagram ◽  
State Transition Diagram

This paper presents a method for test scenario generation based on formal specifications and usage profiles. It is a major component of a framework for testing object-oriented programs. In this framework, the requirements of a software system are formally specified. The anticipated application of the system is expressed in a usage profile, which is a state model that indicates the dynamic behavior of the system and execution probabilities for the behaviors. The state model is used as a guide to derive the anticipated operation scenarios. An enhanced state transition diagram is used to represent the state model, which incorporates hierarchy, usage and parameter information. Since the number of feasible scenarios can be extremely large, probability and importance criteria are used to select the most probable and important scenarios.

scholarly journals Mutated Specification-Based Test Data Generation with a Genetic Algorithm

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 331
Author(s):  
Rong Wang ◽  
Yuji Sato ◽  
Shaoying Liu
Keyword(s):  
Genetic Algorithm ◽  
Test Data ◽  
Test Cases ◽  
Formal Specifications ◽  
Data Generation ◽  
Testing Methods ◽  
Functional Changes ◽  
Target Program ◽  
Generate Test Data

Specification-based testing methods generate test data without the knowledge of the structure of the program. However, the quality of these test data are not well ensured to detect bugs when non-functional changes are introduced to the program. To generate test data effectively, we propose a new method that combines formal specifications with the genetic algorithm (GA). In this method, formal specifications are reformed by GA in order to be used to generate input values that can kill as many mutants of the target program as possible. Two classic examples are presented to demonstrate how the method works. The result shows that the proposed method can help effectively generate test cases to kill the program mutants, which contributes to the further maintenance of software.

scholarly journals On the Expressive Power of Some Extensions of Linear Temporal Logic

2018 ◽  
Vol 25 (5) ◽  
pp. 506-524
Author(s):  
Anton Gnatenko ◽  
Vladimir Zakharov
Keyword(s):  
Temporal Logic ◽  
Reactive Systems ◽  
Expressive Power ◽  
Linear Temporal Logic ◽  
Reactive System ◽  
Formal Specifications ◽  
Control Signals ◽  
Finite State ◽  
Finite State Transducer ◽  
Output Alphabet

One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals and compositions of basic actions performed by the system. We believe that the behaviour of this kind requires more suitable and expressive means for formal specifications than the conventionalLT L. In this paper, we define some new (as far as we know) extensionLP-LT Lof Linear Temporal Logic specifically intended for describing the properties of transducers computations. In this extension the temporal operators are parameterized by sets of words (languages) which represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of the temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of the transducer to the specified environmental influences. In our earlier papers, we considered a model checking problem forLP-LT LandLP-CT Land showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power ofLP-LT Lby comparing it with some well known logics widely used in the computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1-LT Lof our logic is more expressive thanLTLand another restricted variantLP-n-LT Lhas the same expressive power as monadic second order logic S1S.

Online Testing of Nondeterministic Systems with the Reactive Planning Tester

2012 ◽  
pp. 113-150 ◽  
Author(s):  
Jüri Vain ◽  
Marko Kääramees ◽  
Maili Markvardt
Keyword(s):  
Wide Spectrum ◽  
Shortest Paths ◽  
Planning Horizon ◽  
Online Testing ◽  
Optimal Test ◽  
Control Loops ◽  
Model Based ◽  
Reactive Planning ◽  
Implementation Under Test ◽  
Finite State

We describe a model-based construction of an online tester for black-box testing. Contemporary model-based online test generators focusing mainly on computationally cheap but far from optimal planning strategies cover just a fraction of the wide spectrum of test control strategies. Typical examples of those used are simple random choice and anti-ant. Exhaustive planning during online testing of nondeterministic systems looks out of reach because of the low scalability of the methods in regard to the model size. The reactive planning tester (RPT) studied in this chapter is targeted to fill the gap between these two extremes. The key idea of RPT lies in offline static analysis of the IUT (implementation under test) model to prepare the data and constraints for efficient online reactive planning. The external behavior of the IUT is modelled as an output observable nondeterministic EFSM (extended finite state machine) with the assumption that all the transition paths are feasible. A test purpose is attributed to the transitions of the IUT model by a set of Boolean variables called traps that are used to measure the progress of the test run. We present a way to construct a tester that at runtime selects a suboptimal test path from trap to trap by finding the shortest path that covers unvisited traps within planning horizon. The principles of reactive planning are implemented in the form of the decision rules of selecting the shortest paths at runtime. Based on an industrial scale case study, namely the city lighting system controller, we demonstrate the practical use of the RPT for systems with high degree of nondeterminism, deep nested control loops, and requiring strictly bounded tester response time. Tuning the planning horizon of the RPT allows a trade-off to be found between close to optimal test length and scalability of tester behavior with computationally feasible expenses.

scholarly journals Test Case Classification using Category-Partition Finite State Machine

1970 ◽  
Vol 3 (1) ◽  
pp. 17-21
Author(s):  
Penpicha Suphapala ◽  
Umaporn Leelanuntakul ◽  
Nuchakorn Ngamsaowaroj ◽  
Peraphon Sophatsathit
Keyword(s):  
Finite State Machine ◽  
State Machine ◽  
Test Case ◽  
Test Cases ◽  
Software Development Process ◽  
Test Scenario ◽  
Finite State ◽  
Input Domain ◽  
Test Process ◽  
Case Classification

Testing is an essential activity in software development process. Testers and developers alike are facing a formidable expectation of delivery bug-free software. Certifying bug-free with exhaustive test is commonly known to be impossible. Numerous efforts have been attempted to arrive at a plausible test scenario wherein thorough coverage can be attained. Conventional approaches usually require large amount of test data (or input domain) to generate necessary test cases at premium expenses which, in many cases, end up to be a recalcitrant test process. This paper proposes a straightforward, yet practical algorithmic method to reduce all relevant test cases. The central idea rests upon identifying the relationships among category partition of input specifications and program constraints that are subsequently employed to construct a finite state machine. As such, all paths connecting the start and end states represent the required test cases. Reduction on the number of generated test frames based on the proposed method in comparison with conventional approaches proves to be quite significant.

Sign in / Sign up

Export Citation Format

Share Document