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 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.
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.
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.
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.
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 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.
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.
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 (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.
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 – 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.
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.
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.
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.
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.
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 provides the means to describe program defects as AST sub-trees (derived from C/C++, Java and C# programs).
Avalanche tool is based on Valgrind dynamic instrumentation framework and perform automatic critical runtime defect detection through iterative analysis.
Noon is an easily extensible framework for semantic search and exploration of domain-specific information.
API Gateway provides more than 25 tools based on natural language processing, social networks analysis, and knowledge base utilization.
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 is a toolkit for testing applications developed in C. CTESK implements UniTESK concepts of automated testing based on specifications.
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).
System of management requirements Requality is tool for working with requirements, especially for software systems.
JavaTESK is a toolkit for testing applications developed in Java.
PyTESK is a technology of software testing based on formal specifications.
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 (Semantics Testing Kit) is an automatic method for generation of test sets for a translator front end.
OTK (Optimizer Testing Kit) is an automated test development tool for software using complex data structures.
SynTESK (Syntax Testing Kit) is a toolkit for testing parsers of formal languages.
RaceHound is a software for data race detection in Linux kernel modules.
Open Source Technologies
Participating in development of Apache Spark and using it in own projects.
Static instrumentation tool allows to modify ARM ELF executables and shared libraries to change or extend functionality.
KEDR is a framework for dynamic (runtime and post factum) analysis of Linux kernel modules, including device drivers, file system modules, etc.