Abstract:

This paper presents the experience of verifying client implementations of the TLS cryptographic protocol version 1.3. TLS is a widely used cryptographic protocol today, designed to create secure data transmission channels. The protocol provides the necessary functionality for its tasks: confidentiality of transmitted data, data integrity, and authentication of the parties. In the new version 1.3 of the TLS architecture was significantly redesigned, eliminating a number of shortcomings of previous versions that were identified both during the development of implementations and during their operation. We used a new test suite for verifying client 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. 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. 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. The current work is part of the TLS 1.3 protocol verification project and covers TLS client implementations.

Abstract:

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.

Abstract:

The article describes new approaches related to the collection of data from heterogeneous information systems of access to scientific publications using open international standards and protocols for the formation of systems of open access to scientific geological publications. Based on developed and adapted approaches and technological solutions, a set of programs of information and analytical system of access to scientific publications has been implemented, implementing functions of collection, search, cataloguing, filtering and management of scientific publications and their metadata.

Abstract: When deriving tests for checking functional and nonfunctional requirements for components of control systems, the notion of separablity becomes very important that is used for distinguishing the fault-free component from a faulty one. In order to do this, proper separating sequences are utilized. Such sequences are well studied for complete and deterministic Finite State Machines but components of control systems can be only partially described and their behavior can be nondeterministic. In this paper, we consider the formal model of Input/Output automata, introduce the notion of a separating sequence for two such automata and propose an approach for deriving such a separating sequence.

Abstract: Virtual research centre of digital preservation in Europe provides a natural basis for long-term consolidation of digital preservation research and expertise. Spatial Data Infrastructure will cover technical methods for preservation, access and most importantly re-use of data holdings over the whole lifecycle; legal and economic issues including costs and governance issues as well as digital rights; and outreach within and outside the consortium to help to create a discipline of data curators with appropriate qualifications. Main tasks of Spatial Data Infrastructure SDI development are building global infrastructure for IT and geodata; satellite information harmonization; usage of agreed upon set of standards; clear documentation describing the parts of the system; interoperability between independently created applications and databases; common standards within their interfaces, protocols and data formats; and finally support of a general data policy for data creation, access, and support of satellite information. Fundamental principle of Russian segment of SDI is providing interoperability – the ability of interaction for heterogeneous services and data catalogues within the bounds of a unified informational system. The Russian segment of distributed informational system has been built on the basis of EOLI-XML and SSE technologies.

Abstract:

An analysis of the speed and efficiency of data transfer using the WebSocket and REST API protocols was carried out. To compare the speed of processing stream objects and identify a more reliable technology for developing APIs, expansions of basic functions in Taylor and Fourier series were used. As a result, it was revealed that the REST API is a faster and more accessible resource for transmitting information data in a bitwise transformation, and the scalability of this protocol prevails in the number of processed units, which allows expanding the number of tests performed.