Ivannikov Institute for System Programming of the RAS


Download catalogue of technologies

Innovations

Asperitas and cloud solutions family

Asperitas is a platform for data storage and performing complex resource-intensive calculations on demand. It includes a cloud environment also called Asperitas (listed as No. 5921 in the Unified Register of Russian Programs) as well as Michman, a PaaS orchestrator, and Clouni, an IaaS orchestrator. Fanlight, a web laboratories platform, is also a part of ISP RAS cloud solutions family (listed in the Register as No. 6066).

Astraver Verification Toolset

AstraVer Toolset is a deductive verification system for key software components. It allows developing and verifying security policy models as well as proving the correctness of software modules written in the C programming language. AstraVer is essential for ensuring the required trust levels from ADV_SPM and ADV_FSP assurance families as defined in the ISO/IEC 15408 standard.

BinSide: a binary code static analysis tool

BinSide is a static program analysis platform for finding defects in binary code. It is useful when checking programs without source code, such as closed source 3rd party libraries, as well as assisting with required static information to dynamic analysis tools.

Casr: crash analysis and severity reporting tool

Casr creates automatic reports for crashes happened during program testing or deployment. The tool works by analyzing Linux coredump files. The resulting reports contain the crash’s severity and additional data that is helpful for pinpointing the error cause.

Constructivity 4D: a technology of indexing, searching and analysis of large spatial-temporal data

Constructivity 4D is a technology for creating innovative software services that are capable of processing highly dynamic scenes and vast arrays of spatial and temporal data. It performs visual analysis of millions of objects with individual geometry and dynamic behavior. Constructivity is deployed within the Synchro system (Bentley Systems) that is used for 4D modeling of extremely large construction sites.

Dedoc: a document structure retrieval system

Dedoc is an open universal system for converting documents to a unified format. It extracts a document’s logical structure, its tables and metadata. The document’s contents are represented as a tree storing headings and lists of any level. Dedoc can be integrated in a document contents and structure analysis system as a separate module.

DigiTEF: a digital twin platform

DigiTEF is a software platform based on OpenFOAM and other open source tools, as well as unique modules and libraries developed at ISP RAS. DigiTEF solves various application problems of gas dynamics, aerodynamics, hydrodynamics, and acoustics. It is tailored for creating and working with highly sophisticated digital models of industrial devices. DigiTEF is included in the Unified Register of Russian Programs (No. 5377).

Docmarking: a system for marking text documents

Docmarking is a unique system for embedding digital watermarks into text documents. It allows creating a digital or physical document copy that is almost indistinguishable from the original yet exactly identifies the user or the device that was the intended recipient.

Klever: a verification framework for models of industrial software

Klever is a framework for verifying models that are automatically extracted from large software systems’ source code written in the C programming language. Klever allows specifying various security and safety requirements and verifying them automatically with the preconfigured precision level.

Lingvodoc: a virtual laboratory for documenting endangered languages

Lingvodocis a system intended for collaborative multi-user documentation of endangered languages, for creating multi-layered dictionaries and performing scientific work with the received sound and text data. It is a joint project with the Institute of Linguistics of the Russian Academy of Sciences and Tomsk State University. Lingvodoc is under active development since 2012.

MASIW: support for designing highly reliable software systems

MASIW is a toolset for developing highly reliable hardware and software systems for avionics, medicine, and other safety critical areas. It is designed for engineers creating airborne hardware/software systems that are developed using the integrated modular avionics (IMA) approach. MASIW can be easily adapted for other application areas.

MicroTESK: a test program generator

MicroTESK is a reconfigurable and extendable framework for generating test programs for functional verification of microprocessors. MicroTESK allows automatically constructing test program generators based on formal specifications of microprocessor architectures. MicroTESK supports a wide range of architectures including RISC, CISC, VLIW, and DSP. MicroTESK supports online test program generation.

Protosphere: a network traffic analyzer

Protosphere is a system of deep packet inspection (DPI). It can serve as a part of intrusion and information leak protection systems. Protosphere detects inconsistencies between a protocol specification and the actual traffic. It allows you to add support quickly for new protocols (either open or closed) due to the flexibility of its internal representation.

Retrascope: static analysis of hdl descriptions

Retrascope is a functional verification toolkit for digital hardware designs. Retrascope provides automated engines for code analysis, formal model extraction and functional test generation. The toolkit accepts digital hardware module descriptions as inputs, written on the synthesizable subset of Verilog and VHDL languages, as well as their behavioral specifications.

SciNoon: exploratory search system for scientific groups

SciNoon is a system for collaborative exploration of scientific papers. SciNoon is an essential tool for a group of researchers to dive quickly into the new area of knowledge and to find answers on their questions, following up with tracking new research on the topic of interest with highly customizable alerts.

Svace static analyzer

Svace is an essential tool of the secure software development life cycle, the main static analyzer that is used in Samsung Corp. It detects more than 50 critical error types as well as hundreds of coding issues. Svace supports C, C++, C#, Java, Kotlin, and Go. Svace is included in the Unified Register of Russian Programs (No.4047).

Talisman: a data processing framework

Talisman is a unified set of tools that automate typical data processing tasks, such as data retrieval, integration, analysis, storage and visualization. It makes possible the fast development of specialized multi-user analytical systems that merge and work uniformly with the data from private databases and Internet sources (including social networks).

Texterra: a semantic analyzer

Texterra — is a scalable platform for extracting semantics from text. It contains the complete fundamental set of technologies for creating multifunctional applications for text analysis. Texterra bases its semantic analysis approach on concept identification. The platform is included in the Unified Register of Russian Programs (No.4048).

Safe compiler

The safe compiler avoids introducing new vulnerabilities in program’s binary code w.r.t. its source code when aggressively optimizing (e.g., when making use of source code constructs exhibiting undefined behavior). The compiler tries to restrict optimizations as little as possible, which allows avoiding the large performance drop compared to the solution with all optimizations turned off.

ISP Crusher: a dynamic analysis toolset

ISP Crusher is a toolset that combines various dynamic analysis approaches. It includes ISP Fuzzer, a fuzzing tool, and Sydr, an automatic test generation tool for complex programs. In the near future Crusher will also include the BinSide analyzer, another ISP RAS technology. Crusher allows organizing a development process that is fully compliant with GOST R 56939-2016 and other regulatory requirements of FSTEC of Russia.

ISP Obfuscator

Obfuscator is a set of technologies to prevent mass exploitation of vulnerabilities resulting from errors or backdoors. In case a hacker has attacked one of the devices that has a certain software installed, the rest will remain protected by changes to the code that the tool made.

ISP RAS software analysis platform based on QEMU

ISP RAS Foundation Platform for creating program analysis systems is built on top of open source QEMU emulator. This framework is essential for organizing cross platform development. It supports reverse debugging and introspection features, as well as full system emulation mode for debugging low-level software.

Construtivity. The technology of indexing, searching and analysis of large spatio-temporal data

The rapid growth of information volumes, as well as the need for its analysis and interpretation, leads to the development of new approaches to the management of multidimensional data and, in particular, to the management of spatiotemporal data. Usually popular general-purpose database management systems provide spatial indexing and retrieval tools for such purposes, which successfully manage processing of static information, but are not adapted for data liable to permanent changes. In turn, temporal systems are oriented to work with the data that has a history of changes, but do not take into account spatial factors. The problem of data management is even more complicated when they are not just arrays of points in a multidimensional space, but complex structures, for example, a set of mobile objects with extended boundaries and imposed composition relations.

LDV. A technology for static verification of Linux kernel drivers

Bugs in Linux kernel drivers directly affect security, reliability and performance of the kernel and user space applications. Code review, automated testing and static analysis allows detection quite a lot of bugs in Linux kernel drivers. However, just static verification aims at identifying all bugs of a particular type. Configurable framework for static verification of Linux kernel drivers LDV KLEVER provides means for automated preparation of source code of drivers for verification on the base of environment model specifications and checking it against correctness rule specifications using static verification tools.

Cloud-Based Development Infrastructure for Russian Tizen Platform

ISP RAS provides cloud infrastructure that supports development lifecycle of Russian Tizen platform. This infrastructure provides tools for community development of the platform components. It enables performing regular automatic builds and testing of Tizen platform images, and helps developers to make adaptations of the OS and build Tizen platform images for new hardware architectures.

SharpChecker. Static analysis toolkit for defect detection in C# source code

SharpChecker is the platform for static analysis of C# programs, aimed at finding bugs. The tool contains both a code analyzer engine as well as components ready for integration into industrial development processes. SharpChecker can be used not only by programmers to fix errors in the project, but also by managers as another dynamic metric to evaluate the quality of the product.