Astraver Verification Toolset


Download catalogue of technologies

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.

Features and advantages

AstraVer Toolset is a set of tools designed for industrial use. It is based on many years of scientific research and combines two verification approaches: at the model level and at the code level. Parts of the AstraVer Toolset are similar to Microsoft VCC and Frama-C WP, but unlike those AstraVer is specifically designed to support the key security components’ verification in the Linux kernel. AstraVer Toolset is free and open source, available at http://linuxtesting.ru/astraver.

AstraVer provides:

  • An integrated approach to verification, supporting the formalization of high-level requirements and analyzing the C source code behavior.
  • Modeling and formalizing functional requirements, proving internal consistency and unreachability of insecure states.
  • Testing whether functional requirements are satisfied in an implementation, using their formal models to check the correctness of the observable behavior and to evaluate the quality of testing and generated test cases.
  • Verification of critical components written in C (requirements’ formalization, correctness proof on all possible input values).
  • Support for real industrial C code (GCC compiler extensions, arithmetic operations with bitwise precision, address arithmetic including the container_of intrinsic, function pointers, casting).
  • Adhering to the protection profile requirements (ISO/IEC 15408), such as
    • formal security policy modeling;
    • formal verification of internal consistency of a security policy model;
    • formal proof that a target system cannot reach an insecure state;
    • a formal or a semi-formal functional specification development;
    • a formal/semi-formal proof of correspondence between the security policy model and the functional specification;
    • a formal/semi-formal proof of correspondence between different representations of target software, like functional specification, design and source code.
  • Ability to adjust the toolset for a specific customer to perform the C source code components verification.

Who is AstraVer target audience?

  • Companies developing critical systems, including software in aviation, railway, medical and nuclear power industries.
  • Companies that need to certify their software as guided by the ISO/IEC 15408 standard.
  • Certification laboratories for information protection software.

AtstraVer deployment stories

AstraVer Toolset was used in the development of access control mechanisms for Astra Linux Special Edition (RPA RusBITech JSC). As a result, this Astra Linux edition has passed the certification for compliance with the FSTEC information security requirements, which are defined for operating systems of the 2A protection profile. Both the security policy model and the access control mechanisms source code were successfully verified using AstraVer Toolset. The verification work for the new security model features is constantly ongoing.

AstraVer workflow

Astraver Verification Toolset

Developer/Participant

Software Engineering

Back to the list of technologies of ISP RAS