Institute for System Programming of the Russian Academy of Sciences


Innovations

Own Technologies

Svace Static Analyzer. Finding critical program errors in production within secure development lifecycles

ISP RAS has developed Svace static analysis tool that satisfies all requirements for a production quality analyzer. Svace supports C/C++, Java, and C# programming languages (C# can be also shipped separately as it is implemented as a standalone tool), and it runs on Linux and Windows. Svace analyzes programs that can be built on Intel x86/x86-64 Linux/Windows, ARM/ARM64 architectures. Popular C/C++ compilers for Linux and Windows are supported as well as a range of compilers for embedded systems.

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.

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.

BINSIDE. Static binary code analysis tool

Software developers often face a problem of incorporating complex computations, data encryption and compression algorithms, and similar common notions into their code. This is typically done by using standard libraries specializing in a group of tasks; these libraries are often distributed in binary code only. On the other hand, software maintenance is gradually becoming more and more important within the development cycle; software maintenance incorporates the task of updating both its code and external libraries. External libraries and auxiliary programs, distributed in binary form, need to conform to quality and security standards.

Anxtiety. Dynamic program analysis tool

Dynamic symbolic execution is a method of automatic input data generation for target program without knowledge of its internal structure and semantics; generated input data is used to traverse execution paths and attempt to force defects caused by dangerous operations. Dynamic symbolic execution incorporates a number of steps that are performed iteratively: execute the target program and form an execution path constraint using a set of input data, then process the generated path constraint with the help of a solver in order to construct new sets of input data to reach previously uncovered areas of code or trigger dangerous operations. The most promising set for the next iteration is selected according to the amount of new, previously unknown basic blocks it covers.

Binary Code Analysis Platform Based on QEMU Emulator

QEMU is a full-system multi-target open source emulator. It is widely used for software cross-development. Many large companies (e.g., Google, Samsung, Oracle) prototype and emulate their hardware platforms and peripheral devices on QEMU. QEMU 2.9 emulates 20 different hardware platform families, including x86, PowerPC, Sparc, MIPS, ARM.

ISP Obfuscator. Code obfuscation to protect against vulnerability exploitation

ISP Obfuscator is based on long-term research that ISP RAS started as early as 2002. The obfuscation technology grew up from basic research to industrial deployment. It is covered by dozens of publications and two PhD theses during these years. ISP Obfuscator integrates with compilers to make those transformations transparent for developers. At the moment two compiler infrastructures are supported: LLVM and GCC.

Protosphere. Software platform for deep content inspection with the ability to parse an arbitrary network protocol stack

Nowadays, the task of network traffic analysis is of increasing relevance: the reasons are improvement and deployment of new network technologies (VoIP, P2P, streaming video) and emergence of numerous application level protocols used by new network applications. Offline or online analysis is employed, depending on particular analysis system and the problem being solved.

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.

MicroTESK

MicroTESK (Microprocessor TEsting and Specification Kit) is a framework for generating test programs in assembly language for functional verification of microprocessors. It uses formal specifications as a source of knowledge about the configuration of the microprocessor under verification. Generation tasks are described in a special Ruby-based language which allows formulating verification goals in terms of test situations derived from formal specifications. Such an approach simplifies configuring the framework and improves the level of test coverage. MicroTESK has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors.

Retrascope. Reverse engineering tool for HDL descriptions

HDL Retrascope is a toolkit for reverse engineering and transformation of digital hardware designs described in such HDLs (hardware description languages) as Verilog и VHDL. The toolkit allows analyzing HDL descriptions, reconstructing the underlying models (extended finite state machines, EFSMs) and using the derived models for test generation, property checking and other tasks. HDL Retrascope is organized as an extendable framework with the ability to add new types of models as well as tools for their analysis and transformation. The primary application domain of the toolkit is functional verification of hardware at the unit level.

MASIW. Software tools for development of Integrated Modular Avionics

MASIW – Modular Avionics System Integrator Workplace. This is the development environment providing tools to develop model of modular avionics of aircrafts, tools to performing analyzes of models for compliance to requirements and tools for generation of configurations data and binary images of program code based on models.

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.

Texterra. Technology for automatic ontology construction and semantic text analysis

The basic problem of text analysis is natural language ambiguity: same words can have different meanings depending on the context. Context understanding requires knowledge bases describing real world concepts. Construction of such knowledge bases (or ontologies) is a very resource- and time-consuming task. Texterra technology provides tools for automatic extraction of knowledge bases from partially structured resources, e.g. Wikipedia and Wikidata, and tools for analysis of texts semantics on top of these knowledge bases. Texterra technology is actively applied in research and industrial projects of ISP RAS.

TALISMAN. Social media analysis technology

ISP RAS has developed a number of original methods for social analysis which were combined into a technology called TALISMAN. Unlike most existing solutions for social analytics, TALISMAN technology was originally aimed at working with large amounts of data. The most promising open solutions from the stack of Big Data technologies are employed, such as: Apache Spark, GraphX, MLLib, etc.

Free Software Based and ISPRAS Developed Cloud IaaS Solutions

Cloud infrastructure can significantly reduce resources and development time by optimizing the use of resources and reducing the time required to deploy and configure systems. For example, the load of web-services with a large number of users can drastically change depending on the time of the day, the time of the year and events (such as the Christmas Day). With elastic balancing of resources in the cloud environment, it is possible to save a huge amount of resources. The cloud infrastructure of ISP RAS consists of several components based on the most promising technologies that provide virtualization and reliable storage.

AstraVer Toolset. Deductive verification of Linux kernel modules and security policy models

Software plays a key role in many systems, e.g., safety-, security-, and missioncritical systems. Bugs in such software can lead to catastrophic consequences. As a result development of critical software is regulated by certification standards/guidelines (like DO-178С, ISO/IEC 15408, etc) that require following best practices in development process.

KAST: Defect description AST-pattern language

KAST provides the means to describe program defects as AST sub-trees (derived from C/C++, Java and C# programs).

Avalanche: dynamic program analysis tool

Avalanche tool is based on Valgrind dynamic instrumentation framework and perform automatic critical runtime defect detection through iterative analysis.

Noon - framework for semantic search and exploration of domain-specific information

Noon is an easily extensible framework for semantic search and exploration of domain-specific information.

API Gateway - a platform for load-balancing

API Gateway provides more than 25 tools based on natural language processing, social networks analysis, and knowledge base utilization.

Sedna - Native XML Database System

Full-featured native XML DBMS with support for the W3C XQuery language. XML is standard for storing and exchanging information in the Web. In order to facilitate work with big amount of XML data we developed special DBMS system that is called Sedna.

CTESK

CTESK is a toolkit for testing applications developed in C. CTESK implements UniTESK concepts of automated testing based on specifications.

C++TESK

C++TESK Testing ToolKit is an open-source C++ based toolkit intended for automated functional testing of software components (mostly in C/C++) and RTL (HDL) models of digital hardware (in Verilog and VHDL).

Requality

System of management requirements Requality is tool for working with requirements, especially for software systems.

JavaTESK

JavaTESK is a toolkit for testing applications developed in Java.

PyTESK

PyTESK is a technology of software testing based on formal specifications.

UniTESK

UniTESK is a technology for testing application program interfaces (API) which is primarily designed for unit testing.
UniTESK stands for Unified TEsting Specification based toolKit. UniTESK uniformity is provided by the fact that the common testing methodology and general architecture can be implemented for testing modules written in almost all programming languages. Currently there are UniTESK implementations for such languages as C (CTESK), C++ (C++TESK), Java (JavaTESK and Summer), Python (PyTESK).

SemaTESK

SemaTESK (Semantics Testing Kit) is an automatic method for  generation of test sets for a translator front end.

OTK

OTK (Optimizer Testing Kit) is an automated test development tool for software using complex data structures.

SynTESK

SynTESK (Syntax Testing Kit) is a toolkit for testing parsers of formal languages.

RaceHound

RaceHound is a software for data race detection in Linux kernel modules.

Open Source Technologies

Apache Spark - a fast and general engine for large-scale data processing

Participating in development of Apache Spark and using it in own projects.

Other technologies

Static ARM binary code instrumentation

Static instrumentation tool allows to modify ARM ELF executables and shared libraries to change or extend functionality.

KEDR

KEDR is a framework for dynamic (runtime and post factum) analysis of Linux kernel modules, including device drivers, file system modules, etc.