SRE Assignment No 4

Name: Syed Ahmed Raza

Class/Section: BCSE-3C
Roll No: 152

1. Formal Verification Method

a) Formal verification:
Formal verification methods are defined as methods that aim to prove and
demonstrate that the software under
investigation complies with the requirement
specifications that were put in place during requirement
analysis phase of the Systems Development Life Cycle.
b) Purpose of Use:
In engineering we have methods to validate (i.e., Are we trying to make the
product meet the user’s requirements?) and verify (i.e., Does the product conform
to the validated specification?). In the realm of computer hardware Formal
Verification is a pretty old concept and has been in existence since 1984 with
tools like Verilog and now superseded by tools like System Verilog. Such tools
have become part of the IEEE specifications for designing and verifying
hardware.
However, in the realm of software engineering even though we have had
verification tools that have existed since late the 1980s, it still has not been
standardized nor is in widespread use in comparison to its hardware counterpart.
Even when we see the use of Formal Verification, we can see that it is usually
limited to specific fields like cryptography or communication protocols and is
frequently done by the academic circles.

c) How to Use:
Setting out to verify the whole system and every line of written code, even though
theoretically possible, is a beginner’s mistake. The art of engineering is about
being smart enough to know which corners to cut and which ones not to cut. This
is not an easy task - it takes time, practice and experience to take decisions on
 this. We should also keep in mind writing “verification” for a system is not the
same as writing tests Functional and fuzzing for it. Writing tests and achieving
100% code coverage does not guarantee that the system works as intended and it
is only as good as tests themselves (after all, who tests the unit tests?).
Verification and testing can be considered to be two sides of the same coin and
one complements the other, completing the picture.

d) Application Areas:
Some area of applications that make use of formal verification methods include
verifying a model of Concurrent/Distributed Systems. An example is model
checking of concurrent and distributed systems using SPIN model checker. SPIN
can be used to exhibit design flaws in these systems and help to improve the
design. Formal verification methodologies can be also used to check data
integrity. In validating the design of system on chip (SoC) designs for example
and due to the complex nature of these designs, both formal verification and logic
simulation are used

e) Pros and Cons:

 Pros:
● The development of a formal specification provides insights into and an
understanding of the software requirements and software design. This reduces
requirements errors and omissions. It provides a basis for an elegant software
design.
● Formal software specifications are mathematical entities and may be analysed
using mathematical methods. In particular, it may be possible
to prove specification consistency and completeness. It may also be possible
to prove that an implementation conforms to its specification.
● Formal specifications may be automatically processed. Software tools can be
built to assist with their development, understanding, and debugging
● Formal specifications may be used as a guide to the tester of a component in
identifying appropriate test cases. For example, a
function's preconditions and postconditions can be used to design (black box)
tests, and a class invariant can be useful when testing a class in an object-
oriented system.

 Cons:
● Software management is often conservative and is unwilling to adopt new
techniques for which payoff is not obvious. It is difficult to demonstrate that
 the relatively high cost of developing a formal system specification will
reduce overall software development.
● Some software engineers, particularly those in senior positions, have not been
trained in the techniques needed to develop formal software specifications.
Developing specifications requires a familiarity with discrete mathematics and
logic.
● System customers are unlikely to be familiar with formal specification
techniques. They may be unwilling to fund development activities that they
cannot easily monitor.
● Some classes of software system requirements are difficult to specify using
existing techniques. In particular, current techniques cannot be used to specify
the interactive components of user interfaces

2. Static Analysis Method:

a) Technique Description:
Static code analysis and static analysis are often used interchangeably, along with source
code analysis. 
This type of analysis addresses weaknesses in source code that might lead to
vulnerabilities. Of course, this may also be achieved through manual code reviews. But
using automated tools is much more effective.
Static analysis is commonly used to comply with coding guidelines 

b) Purpose of Use:

Static analysis is generally good at finding coding issues such as:

● Programming errors
● Coding standard violations
● Undefined values
● Syntax violations

● Security vulnerabilities
c) How to use:
The static analysis process is relatively simple, as long as it's automated. Generally, static
analysis occurs before software testing in early development. In the DevOps development
practice, it will occur in the create phases.

Once the code is written, a static code analyzer should be run to look over the code. It
will check against defined coding rules from standards or custom predefined rules. Once
the code is run through the static code analyzer, the analyzer will have identified whether
or not the code complies with the set rules. It is sometimes possible for the software to
flag false positives, so it is important for someone to go through and dismiss any. Once
false positives are waived, developers can begin to fix any apparent mistakes, generally
starting from the most critical ones. Once the code issues are resolved, the code can move
on to testing through execution.

Without having code testing tools, static analysis will take a lot of work, since humans
will have to review the code and figure out how it will behave in runtime environments.
Therefore, it's a good idea to find a tool that automates the process. Getting rid of any
lengthy processes will make for a more efficient work environment.

d) Application Area’s:

There are plenty of static verification tools out there, so it can be confusing to pick the
right one. Software tools will work at a variety of levels. Unit-level tools look at
programs or subroutines. Technology-level tools will test between unit programs and a
view of the overall program. System-level tools will analyze the interactions between unit
programs. And mission-level tools will focus on mission layer terms, rules and processes.
Before committing to a tool, an organization should also make sure that the tool supports
the programming language they're using as well as the standards they want to comply
with.

Embold is an example static analysis tool which claims to be an intelligent software

analytics platform. The tool can automatically prioritize issues with code and give a clear
visualization of it. The tool will also verify the correctness and accuracy of design
patterns used in the code.

e) Pros and cons:

 Pros cons

It can evaluate all the code in an application, False positives can be detected.
increasing code quality.

It provides speed in using automated tools A tool might not indicate what the defect is if
compared to manual code review there is a defect in the code.

Paired with normal testing methods, static Not all coding rules can always be followed,
testing allows for more depth into debugging like rules that need external documentation.
code.

Automated tools are less prone to human Static analysis may take more time than
error. comparable methods.

It will increase the likelihood of finding Static analysis can't detect how a function will
vulnerabilities in the code, increasing web or execute.
application security.

It can be done in an offline development System and third-party libraries may not be

environment. able to be analyzed.

3. Dynamic Analysis Method

a) Technical techniques:
Dynamic analysis, also known as dynamic program analysis, is the evaluation of a program
or technology using real-time data. This method of analysis can be done on a virtual
processor or on a real processor. Instead of taking code offline, vulnerabilities and
 program behavior can be monitored while the program is running, providing visibility into its
real-world behavior. 

b) Purpose of Use:

● Set of techniques to rigorously examine a program based on some criteria during run-time
● Code Coverage Analysis
● Error-seeding and mutation testing, regression testing, other testing
● Program slicing
● Assertions

c) How to Use:
Typically, a dynamic analyzer needs an output specification to compare the actual output to.
Generally speaking, an oracle is the specification against which actual outputs compare their
results. Can be another system, model, person, customer, etc. In the case of black box
testing, the output specification is the oracle.

d) Application Areas:
performance evaluation, self-adaptation control (e.g., online capacity
management), problem simulations, measure- mint and logging of simulation data, analysis of
simulation, based user in- terrace for configuring and running dynamic analyses

e) Pros and Cons:

 Pros:
● Dynamic coding helps in identifying weak areas in a run-time environment
● Dynamic testing supports analysis of applications even if the tester does not
have the actual code.
● It identifies weak areas that are hard to be found with static code analysis
● It allows validating static code analysis findings
● It can be applied with any application

 Cons:
● Automated tools may give a false security that everything is checked
● Automated tools can generate false positives and false negatives
● It is not easy to find a trained professional for dynamic testing
● It is difficult to trace the vulnerability in the code, and it takes longer to fix the
problem. Thus, it becomes costly to fix the errors