Formal Methods Techniques in AI Verification

Formal methods are mathematical techniques used to rigorously verify the correctness, safety, and robustness of AI systems, particularly in high-stakes applications such as autonomous vehicles, medical diagnostics, and aerospace. 

When I did my master's degree 10 years ago, I discussed, evaluated, and qualitatively reviewed some of these techniques within the formal methods. You may search my thesis title "A source code perspective C overflow vulnerabilities exploit taxonomy based on well-defined criteria"

Below is a brief explanation of key techniques within formal methods, along with relevant examples and mathematical formulations simplified to ease the understanding.

---

1. Abstract Interpretation

Definition:
Abstract interpretation is a static program analysis technique that approximates program behavior by mapping infinite concrete domains (e.g., real numbers) to a finite abstract domain (e.g., intervals). This technique is used to detect errors such as buffer overflows, division by zero, and numeric instability.

Example:
Consider an AI algorithm using floating-point arithmetic. Instead of testing all possible floating-point values, abstract interpretation groups them into intervals. If a neural network's activation function outputs values in $[-1,1]$, the abstract interpretation would ensure no computations exceed this range.

Mathematical Representation:
For a program function $f(x)$, abstract interpretation defines an abstraction function $\alpha$ and a concretization function $\gamma$:

$$\forall x \in \text{ConcreteDomain}, \quad \alpha(f(x)) \approx f(\alpha(x))$$

where $\alpha(x)$ is the abstract representation, and $\gamma(\alpha(x))$ maps it back to the concrete domain.

---

2. Semantic Static Analysis

Definition:
Semantic static analysis inspects a program's source code without executing it to determine properties such as termination, correctness, and possible runtime errors.

Example:
A neural network classifier trained for medical diagnosis should not output probabilities exceeding $1$. Static analysis verifies whether the probability function adheres to:

$$\sum P(y|x) = 1, \quad \forall x \in \text{InputDomain}$$

where $P(y|x)$ represents the probability of class $y$ given input $x$.

---

3. Model Checking

Definition:
Model checking systematically explores a system's state space to ensure it satisfies a given set of formal specifications, typically expressed in temporal logic.

Example:
In an autonomous driving system, a model checker can verify whether a car always stops at a red light by checking the Linear Temporal Logic (LTL) formula:

$$\Box (\text{RedLight} \rightarrow \Diamond \text{Stop})$$

which states that if a red light appears, the car must eventually stop.

---

4. Proof Assistants

Definition:
Proof assistants are software tools that help construct formal proofs of system correctness by allowing users to define mathematical models and verify logical statements interactively.

Example:
A self-driving car’s braking system should ensure that stopping distance does not exceed a threshold $d_{\text{safe}}$:

$$d_{\text{stop}}=\frac{v^2}{2a}\le d_{\text{safe}}$$

where $v$ is the vehicle speed and $a$ is the braking deceleration. A proof assistant like Coq or Isabelle verifies this inequality.

---

5. Deductive Verification

Definition:
Deductive verification formally proves that a system satisfies its specification using logical reasoning. This involves deriving proof obligations that demonstrate correctness.

Example:
In an AI-based medical diagnosis system, a deductive verification approach ensures that if input $x$ is classified as disease-positive, then the treatment $T(x)$ should always be prescribed:

$$\forall x, \quad \text{Diagnosis}(x) = \text{Positive} \Rightarrow T(x) \neq \emptyset$$

---

6. Model-Based Testing

Definition:
Model-based testing (MBT) derives test cases from formal models of a system’s expected behavior, ensuring comprehensive test coverage.

Example:
For an AI-powered ATM system, a state machine model might specify:

1. Insert Card → PIN Entry → Transaction → Dispense Cash
2. Insert Card → PIN Entry → Incorrect PIN → Card Ejection

Each path is converted into test cases, ensuring all scenarios are tested.

---

7. Design by Refinement

Definition:
Design by refinement incrementally develops a system by starting with an abstract specification and progressively introducing more details while maintaining correctness.

Example:
For a neural network-based control system, an initial specification may state:

$$\text{Output}\in [0,1]$$

As the design is refined, more constraints are added to ensure robustness against adversarial attacks.

---

Conclusion

These formal methods provide robust frameworks for ensuring AI systems behave as expected in critical applications. While abstract interpretation and static analysis focus on pre-runtime validation, model checking, and proof assistants help verify properties at runtime. Deductive verification ensures correctness by logical reasoning, while model-based testing and refinement guide structured system development.

Read More

Ontology Model for C Overflow Vulnerabilities Attack

Prepared the slide and was hoping to present at a conference. Unfortunately, due to Covid-19, it can only be shared online here.

I would like to thank all in the slide for making it through especially Saiful who give it all to complete the paper and published it at IJATCSE.

You may access and view the slide at Slideshare

Ontology model for c overflow vulnerabilities attack from Nurul Haszeli Ahmad

#covid19 #overflow #softwaresecurity #overflowvulnerabilities #programanalysis #staticanalysis #informationsecurity #security #cybersecurity

Read More

List of available data set for Data Scientist

I am exploring on data related to 2019nCoV and found the following list of dataset that can be used for data scientist, data scientist to be, student, etc to explore. Check it out

1. https://data.world/
2. https://quantumstat.com/dataset/dataset.html
3. https://www.ncbi.nlm.nih.gov/labs/virus/vssi/#/virus?SeqType_s=Nucleotide&VirusLineage_ss=Wuhan%20seafood%20market%20pneumonia%20virus,%20taxid:2697049
4. https://www.ncbi.nlm.nih.gov/genbank/2019-ncov-seqs/?utm_campaign=wuhan_nCoV&utm_source=twitter&utm_medium=referral
5. https://www.ncbi.nlm.nih.gov/nuccore/MN908947,MN970003,MN970004,MN938384,MN938385,MN938386,MN938387,MN938388,MN938389,MN938390,MN975262,MN975263,MN975264,MN975265,MN975266,MN975267,MN975268,MN985325,MN988713,MN994467,MN994468,MN997409,MN988668,MN988669
6. https://researchguides.uic.edu/c.php?g=252253&p=1683071
7. https://archive.org/details/2019-search-engine-keyphrases.json

or you can just use google and search the entire internet through the engine
https://datasetsearch.research.google.com/

Read More

Catch Overflows vulnerabilities in C causes by pointer - A tutorial

Kittur Ganesh, Technical Consulting Engineer for Intel Software Development Products, explains how
Pointer Checker – a feature of Intel Parallel Studio XE automates detection and protects against out-of-
bounds memory accesses, facilitating debugging, preventing data corruption, and, when enabled in testing runtimes, exposing issues that might cause exploitable exceptions before release. This tutorial was summarized by John Jainschigg, Geeknet Contributing Editor, from an Intel video webinar (51:39)

Check it out the full tutorial here.

Read More

Memory Overflow: C versus Java

Memory overflow (a.k.a buffer overflow, buffer overrun, overflow) is a vulnerability in applications causes by programming errors or ignorant of security by developers [1], [2], [3]. Memory overflow is a vulnerability whereby an attackers or hackers can exploit a code in programs that can trigger overflow in Computer's memory system (stack, heap, BSS, and data segment) [4], [5], [6], [7], [8], [9]. Between all programming, this issue is significant in C and Java [10], [11], [12], [13]. Between C and Java, the issue is more critical in C than Java [14], [15], [16]. Table below shows the comparison that I've done between those two.

Table 1: C versus Java

References:

[1] Viega, J., & McGraw, G. (2002). Building Secure Software: How to Avoid Security Problems the Right Way (2nd Printing ed.). Addison-Wesley.

[2] Seacord, R. (2005). Secure Coding in C and C++. United States of America: Addison-Wesley Professional.

[3] Kaspersky Lab ZAO. (n.d.). Software vulnerabilities . Retrieved November 19, 2011, from Securelist: http://www.securelist.com/en/threats/vulnerabilities?chapter=35

[4] Sycracuse University. (2011). Buffer-Overflow Vulnerabilities and Attacks.

[5] Kratkiewicz, K., & Lippmann, R. (2005). A Taxonomy of Buffer Overflows for Evaluating Static and Dynamic Software Testing Tools. NIST Workshop on Software Security Assurance Tools, Techniques, and Metrics. Long Beach, California.

[6] Fayolle, P. -A., & Glaume, V. (2002). A Buffer Overflow Study: Attacks and Defenses. Unpublished, SecurityFocus.

[7] Kundu, A., & Bertino, E. (2011). A New Class of Buffer Overflow Attacks. Proceedings of the 2011 31st International Conference on Distributed Computing Systems (pp. 730 - 739). Minneapolis: IEEE Computer Society.

[8] Conover, M., & Team, w. S. (1999, January). w00w00 on Heap Overflows. Retrieved November 28, 2011, from CGSecurity: http://www.cgsecurity.org/exploit/heaptut.txt

[9] Shao, Z., Zhuge, Q., He, Y., & Sha, E. H.-M. (2003). Defending Embedded Systems Against Buffer Overflow via Hardware/Software. Proceedings of the 19th Annual Computer Security Applications Conference. Washington, DC, USA: IEEE Computer Society.

[10] Cenzic Inc. (2009, November 9). Cenzic Web Application Security Trends Report Shows Increase in Hacker Attacks on Web Sites Exploiting Faults in Popular Web Browsers and Software. Retrieved January 30, 2011, from http://www.cenzic.com/pr/200911091/

[11] MITRE Corporation. (2012). Vulnerability Search. Retrieved January 10, 2012, from CVE Details - The ultimate security vulnerability datasource: http://www.cvedetails.com/vulnerability-search.php

[12] MITRE Corporation. (2012). Vulnerability Search - Java Overflow. Retrieved January 10, 2012, from CVE Details - The ultimate security vulnerability datasource: http://www.cvedetails.com/vulnerability-search.php?f=1&vendor=&product=Java&cveid=&cweid=&cvssscoremin=&cvssscoremax=&psy=&psm=&pey=&pem=&usy=&usm=&uey=&uem=&opdos=1&opec=1&opmemc=1&opov=1

[12] Mandalia, R. (2011, December 07). Microsoft Holds Java Vulnerabilities Responsible in Nearly Half of All Attacks. Retrieved January 10, 2012, from ITProPortal - 24/7 Tech Commentary & Analysis: http://www.itproportal.com/2011/12/07/microsoft-holds-java-vulnerabilities-responsible-nearly-half-all-attacks/

[14] Baker, & Graeme. (2008, January 11). Schoolboy hacks into city's tram system. Retrieved November 17, 2011, from The Telegraph: http://www.telegraph.co.uk/news/worldnews/1575293/Schoolboy-hacks-into-citys-tram-system.html

[15] Chen, T. M. (2010). Stuxnet, the Real Start of Cyber Warfare. IEEE Network , 24 (6), 2 - 3.

[16] Carty, D. (2010, February 3). Apple's Wozniak: Toyota Has Software Problem. (CBS Interactive Inc) Retrieved November 18, 2011, from CBS News: http://www.cbsnews.com/8301-503983_162-6169804-503983.html

[17] One, A. (1996). Smashing the Stacks for Fun and Profit. Phrack Magazine , 7 (49).

[18] Viega, J., Bloch, J., Kohno, Y., & McGraw, G. (2000). ITS4: a static vulnerability scanner for C and C++ code. 16th Annual Conference of Computer Security Applications (ACSAC), (pp. 257 - 267). New Orleans, LA , USA.

[19] Krsul, I. V. (1998). Software Vulnerability Analysis. Phd Thesis, Purdue University.

 [20] Alhazmi, O. H., Woo, S. W., & Malaiya, Y. K. (2006). Security Vulnerability Categories in Major Software Systems. 3rd IASTED International Conference on Communication, Network, and Information Security (CNIS), (pp. 138 - 143).

[21] Howard, M., LeBlanc, D., & Viega, J. (2010). 24 Deadly Sins of Software Security - Programming Flaws and How to Fix Them. McGraw-Hill.

[22] Howard, M., LeBlanc, D., & Viega, J. (2005). 19 Deadly Sins of Software Security - Programming Flaws and How To Fix Them. Emeryville, California, USA: McGraw-Hill/Osborne.

[23] Andersen, L. O. (1994). Program Analysis and Specialization for the C Programming Language. PhD Thesis, University of Copenhagen, Computer Science Department.

[24] National Institute of Standards and Technology. (2012, 16 01). Vulnerability Summary for CVE-2012-0266. Retrieved 16 01, 2012, from National Vulnerability Database: http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2012-0266

[25] Open Source Vulnerability Database (OSVDB). (2012, 01 11). 78252 : NTR ActiveX Control Boundary Error Multiple Method Parameter Handling Overflow . Retrieved 01 16, 2012, from OSVDB: http://osvdb.org/show/osvdb/78252

[26] National Institute of Standards and Technology. (2008, October 09). Vulnerability Summary for CVE-2000-0146. Retrieved January 10, 2012, from National Vulnerability Database: http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2000-0146

[27] IBM X-Force. (2011). IBM X-Force 2010 Trend and Risk Report. Technical Report, IBM.

 [28] Martin, B., Brown, M., Parker, A., & Kirby, D. (2011, September 13). 2011 CWE/SANS Top 25 Most Dangerous Software Errors. (S. Christey, Ed.) Retrieved September 28, 2011, from Common Weakness Enumeration (CWE): http://cwe.mitre.org/top25/

 [29] HewlettPackard. (2011). 2010 Full Year Top Cyber Security Risks Report - In-depth analysis and attack data from HP DVLabs. Technical Report, HP.

 [30] Cenzic Inc. (2010, March 2). Cenzic Web Application Security Trends Report Reveals 90 Percent of Web Applications Vulnerable, Adobe One of The Most Vulnerable. Retrieved January 30, 2011, from https://cenzic.com/pr_20100302/

[31] Chechik, D. (2011, December 16). Prevalent Exploit Kits Updated with a New Java Exploit. Retrieved January 10, 2012, from M86 Security Labs: http://labs.m86security.com/tag/java/

[31] Open Source Vulnerability Database (OSVDB). (2012). The Open Source Vulnerability Database. Retrieved January 10, 2012, from OSVDB: http://osvdb.org/

[33] MITRE Corporation. (2012). CVE Details. Retrieved January 10, 2012, from CVE Details: http://www.cvedetails.com

[34] IBM. (2012). Retrieved January 10, 2012, from IBM Internet Security System: http://xforce.iss.net

[35] Secunia. (2012). Retrieved January 10, 2012, from Secunia - Stay Secure: http://secunia.com/advisories/

[36] National Institute of Standards and Technology. (2012). Common Vulnerability Scoring System Version 2 Calculator. Retrieved January 10, 2012, from National Vulnerability Database: http://nvd.nist.gov/cvss.cfm?calculator&version=2

[37] Oracle Corporation. (2010). Secure Computing with Java: Now and the Future. Retrieved January 10, 2012, from ORACLE - Sun Developer Network (SDN): http://java.sun.com/security/javaone97-whitepaper.html

[38] Oracle Corporation. (2012). Java SE Security. Retrieved January 10, 2012, from ORACLE: http://www.oracle.com/technetwork/java/javase/tech/index-jsp-136007.html

[39] Fritzinger, S. J., & Mueller, M. (1996). Java™ Security. White paper, Sun Microsystems, Inc.

[40] Ahmad, N. H., Aljunid, S. A., & Ab Manan, J.-l. (2011). Taxonomy of C Overflow Vulnerabilities Attack. In Z. Jasni Mohamad, W. Mohd, & E.-Q. Eyas (Ed.), International Conferences on Software Engineering and Computer Systems. 180, pp. 376 - 390. Kuantan, Pahang: Springer.

[41] University of Maryland. (2011, December 21). FindBugs™ - Find Bugs in Java Programs. Retrieved January 10, 2012, from FindBugs: http://findbugs.sourceforge.net/

[42] SourceForge.net. (2011, November 04). PMD. Retrieved January 10, 2012, from PMD: http://pmd.sourceforge.net/

[43] Parasoft. (2012). Jtest - Java Static Analysis, Code Review, Unit Testing, Runtime Error Detection. Retrieved January 10, 2012, from Parasoft: http://www.parasoft.com/jsp/products/jtest.jsp/

[44] Coverity, Inc. (2012). Coverity Static Analysis. Retrieved January 10, 2012, from Coverity: http://www.coverity.com/products/static-analysis.html

[45] Henzinger, T. A., Beyer, D., Majumdar, R., & Jhala, R. (2008, 07 11). BLAST: Berkeley Lazy Abstraction Software Verification Tool. Retrieved November 27, 2011, from MTC - Models and Theory of Computation: http://mtc.epfl.ch/software-tools/blast/index-epfl.php

[46] National Science Foundation. (2010, August 4). Retrieved November 25, 2011, from Splint - Annotation Assisted Lightweight Static Checking: http://www.splint.org/

[47] Cousot, P., Cousot, R., Feret, J., Miné, A., & Rival, X. (2006, July 7). The Astrée Static Analyzer. Retrieved November 20, 2011, from The Astrée Static Analyzer: http://www.astree.ens.fr/

[48] MathWorks, Inc. (2011). Retrieved November 18, 2011, from Polyspace Client for C/C++: http://www.mathworks.com/products/polyspaceclientc/?s_cid=global_nav

Read More

10+ free tool for static code analysis

The article was published at Open-Tube.com.

The author list 10+ free tools to analyze source code. The tool are:
Multi-language
1. RATS
2. Yasica

Java
1. CheckStyle
2. FindBugs
3. PMD
4. Hamurapi

C/C++
1. Sparse
2. Splint
3. UNO
4. Blast
5. CPPCheck

Check it out at http://open-tube.com/10-free-tools-for-static-code-analysis/

Read More

Think static analysis cures all ills? Think again.

Mark Pitchford

3/1/2011 11:15 AM EST

Static code analysis has been around as long as software itself, but you'd swear from current tradeshows that it was just invented. Here's how to choose the right code-analysis tools for your project.

Static analysis (or static code analysis) is a field full of contradictions and misconceptions. It's been around as long as software itself, but you'd swear from current trade shows that it was just invented. Static analysis checks the syntactic quality of high-level source code, and yet, as you can tell from listening to the recent buzz, its findings can be used to predict dynamic behavior. It is a precision tool in some contexts and yet in others, it harbors approximations.(read the article here)


I believe none of static analysis tool developer would claim that their tool can solve everything. Don't get the wrong idea, but static analysis is only a tool TO REDUCE (if not remove) software errors and possibility of the software being exploited. And based on my studies (I've published a paper entitled "Preventing Software Vulnerabilities - Why Static Analysis is ineffective"), it is not the tool that failed to deliver or to be blame 100%. The tool is also developed by human which the purpose is to reduce human error in programming. Thus, there will always be limitation on the tool. In addition, the tool are dependent on the technique implemented. Hence, there should be improvement on the technique or combination of multiple technique in a tool first.

Read More

Static Analysis versus Dynamic Analysis

Paul Andersen from GrammaTech (the company that develop CodeSonar) share his thought on using both, static and dynamic analysis, to detect vulnerabilities. (read the articles here)

Lots of comments given which share the same thought as me. However, if I were to choose one, I'll definitely use static analysis. As I'm doing research in that area, I do found that we can remove all vulnerabilities related to C overflows at the beginning without using dynamic analysis. Of course there are pros and cons of using dynamic analysis, but the major issue with dynamic analysis which make me choose static analysis instead of dynamic is that the cost of re-write the code of modified the code is higher after the development phase and it can introduce unknown error too.

However, if a company can afford to use both, then I do recommend to use both. BUT, it is hard to choose the tool as all companies claimed their tool have better detection rate.

Read More

Applying Static Analysis To Medical Device Software

An interesting articles written back on 2008 by David N. Kleidermacher indicates the importance of having static analysis tool to improve reliability and sustainability of medical devices [read here]

However, as complexity increases especially on mobile devices and mission-critical devices like medical and military, static analysis tool is still far away from achieving zero-tolerant or 99.99% secure. It depends on technique and tool use by the tool to statically analyze applications stored in those devices and at the moment, and as written in my paper title "Preventing Exploitation on Software Vulnerabilities: Why Static Analysis Failed?" in WEC 2010, there are more works need to be done to improve static analysis tool capability especially when the complexity and LOC is increase.

Read More

Using static code analysis to support DO-178b certification

Paul Anderson, GrammaTech   
9/6/2011 6:29 PM EDT

In this Product How-To, Paul Anderson of GrammaTech takes you step by step through the DO-178B and how use his company’s static analysis tools to support the safety-critical software requirements of the specification [read more].

As one of my interest in software security, I keen to evaluate the effectiveness and efficiencies of GrammaTech CodeSonar on its static analysis capability using taxonomy of C Overflow Vulnerabilities Attack which I constructed for the purpose of identifying overflow vulnerabilities in C. However, due to fact (based on my email conversation between one of the company's employee), I can't evaluate theirs thus I'm not sure how their tools could help supporting the safety-critical software requirements.

And I can says one things for sure here that all tools including CodeSonar is yet to successfully help in reducing vulnerabilities in software. This can been seen by looking at various vulnerability database and advisories released by Symantec, Karspesky, Microsoft, NIST, etc. The numbers are still large and yet to see it is tremendously reduce.

Read More

The problem with static analyzers

Static analyzers offer a lot of capability. They could easily go a lot further.
At the recent Embedded Systems Conference in Silicon Valley I had the chance to talk to several vendors of static analyzers. These are the tools that evaluate your program to find potential runtime problems, like variables going out of bounds or dereferences of null pointers [read more].

There are few key points here. First, the author mention that static analyzer for embedded is still new and there are still works need to be done in this area especially it is yet to achieve its full capability. Secondly, he mention the limitations or issues related to static analyzer. That was indeed have been carried over for the past decades starting early 90s. There are more than a dozen technique used by static analyzer ranging from as simple as lexical analysis to complex implementation of abstract interpretation. More than 40 tools, open source or commercial version, had been develop based on the 12 techniques. It is yet to produce any significant result in finding errors or problem in the source code.

Read More

http://www.eetimes.com/electrical-engineers/education-training/tech-papers/4135343/Integration-Testing-and-Debugging-of-C-Code-Together-with-UML-Generated-Sources?cid=NL_Embedded&Ecosystem=embedded

Software content has grown rapidly in all manner of safety-critical devices. Meanwhile, society has become increasingly dependent upon their safe operation. Unfortunately, our ability to develop safe and reliable software has not improved at the same rate, resulting in increasing reliability and safety vulnerabilities. This increase in software vulnerability poses a serious threat to human safety and demands new approaches to safe software development. Static analysis has emerged as a promising technology for improving the safety of software in safety critical applications such as medical devices and systems (See Sidebar). Beyond defect prevention, static analysis is also finding a home in medical forensics labs, aiding scientists who must locate the cause of failures in recalled medical devices.

Read more @ EETimes Online
by David N. Kleidermacher

Read More

Why most static analysis tool failed?

Static analysis technique was introduced by King in 1974 as a way to understand and debug program rather than to find vulnerabilities in the program. Static analysis emerges as a major security subject in the year of 2000 after a dissertation by Wagner. Since then, there are more than 40 tools, open-source or commodity, and 11 techniques introduced to the system security world. However, as reported by major security advisors and experts; such as Microsoft Security Advisor, Secania, SANS Institute, and Symantec; vulnerabilities still exist and exploitations are still at large. To this date, there are numerous possibilities and reasons as to why the community is still facing software security issues. One of it is the effectiveness and efficacy of static analysis in preventing these issues.

I'd wrote a paper which discussed on those issues and had proposed ways to overcome the limitation of previous solutions with title "PREVENTING EXPLOITATION ON SOFTWARE VULNERABILITIES – WHY MOST STATIC ANALYSIS IS INEFFECTIVE?" which had been presented in WEC 2010

Anyone interested on that paper may email me here.

Read More

Looking for tool to derive AST from Source Code

I'm looking for a program (or source code written either using java or C language) which be able to take source-code (single or multiple file) and establish AST (abstract syntax tree), PDG (Program Dependency Graph), and CFG (Control Flow Graph).

I've been searching quite sometime but has yet to found any. Most of the tool I found take executable or binary files likes CodeSonar/x86 and IDAPro which does not suite my research.

If any of you know about it, please share the information with me.

Really thankful for all help given :)

Read More