Our focus is on Cloud Quality and Verification. We build technologies and solutions to improve the quality of the cloud computing stack (SaaS, PaaS and IaaS), concentrating on policy management and network security.
Microservices-based architecture is at the heart of many modern cloud applications. In such an architecture, numerous loosely-coupled services communicate over the network using lightweight protocols. To protect sensitive services (e.g., user database) network policies are deployed, restricting the allowed communication channels. These policies can sometimes be tricky to specify, and developers often make mistakes, either blocking essential traffic or opening critical resources to attackers. Our tool, NPV, builds a semantic model for a given set of network policies in a given cluster, and can reason about it. NPV can compare policies, detect common pitfalls and answer queries about allowed/disallowed traffic. It currently supports Kubernetes and Calico.
RuleBase SixthSense Edition
The IBM Formal Verification group develops formal verification solutions for industrial use. Our main asset is RuleBase SixthSense Edition, an industrial strength formal verification platform.
RuleBase SixthSense Edition has been used to formally verify designs in IBM for almost two decades. It is used daily on the hardware projects developed across IBM, running on different design types of different sizes, with different proof algorithms.
RuleBase SixthSense Edition is also available outside of IBM through a licensing process governed by IBM Research. Please contact Eli Arbel for more details on licensing.
Our global team of formal verification experts is pushing the limits of the technology to make RuleBase SixthSense Edition the strongest tool available on the market. The tool is constantly evolving with the addition of cutting edge technology.
RuleBase SixthSense Edition has a simple intuitive interface that makes formal verification accessible to any verification engineer. In IBM and many other companies, formal verification is quickly becoming an inseparable component of the verification flow.
RuleBase SixthSense Edition User Interface
Why Formal Verification?
Simulation used to be the only way to carry out pre-silicon verification. As hardware design complexity grows and the late detection of bugs becomes more expensive, formal-verification (FV) solutions have become a necessity in every hardware design center.
Using adequate FV methodology ensures that a design-under-test is bug free. FV has a fast set up environment and can easily reconstruct bugs that were found in the lab.
What is RuleBase SixthSense Edition
For almost two decades, RuleBase SixthSense Edition has been used by IBM and other companies to formally verify the most critical portions of their hardware designs. IBM's mainline processors, IBM's gaming processors, and many other hardware designs were extensively verified by RuleBase SixthSense Edition. The following make RuleBase the ultimate solution for formal verification:
Power, power, and more power. The strongest formal solution out there.
Ability to handle the largest pieces of logic with the fastest run times.
Support for ABV in the popular assertion languages PSL, SVA.
First on the market with the most powerful model checking algorithms.
Easy to use, easy to implement in an existing verification flow.
Comprehensive package includes everything (compilers, wave viewer, easy GUI, etc).
Personalized customer support.
From Automated Expert mode to a Full-Control Mode
There is no single model checking algorithm which can effectively solve all verification problems. Hence having a reach portfolio of algorithms is key in enabling a formal verification tool to successfully cope with problems of various types, sizes and complexities. RuleBase SixthSense Edition includes a reach set of model checking algorithms (called engines) which run in a transformation-based verification framework (TBV). The TBV framework enables transferring a given model checking problem from one engine to the other while gradually simplifying the problem until it is completely solved. In order to facilitate efficient utilization of the reach set of engines avialable in RuleBase SixthSense Edition, a special Expert Mode engine is available which automatically orchestrates the use of the various engines in a given run. For experienced users a manual mode is also available, in which users build their own configurations of engines using a GUI based configuration manager. A set of pre-defined configurations, each tailored for specific verification scenario (e.g bug hunting) are also provided.