.gitignore

*.aux
*.dvi
*.log
*.pdf

Makefile

RM=rm -f

LATEX=latex
DVIPDFMX=dvipdfmx
DETEX=detex

SOURCES=report3.tex
DVI=$(SOURCES:.tex=.dvi)
PDF=$(SOURCES:.tex=.pdf)

all: pdf
	gnome-open $(PDF)

dvi: $(DVI)

pdf: $(PDF)

.SUFFIXES:
.SUFFIXES: .tex .dvi .pdf

.tex.dvi:
	$(LATEX) $<
	$(LATEX) $<

.dvi.pdf:
	$(DVIPDFMX) $<
	$(DVIPDFMX) $<

.PHONY: wc
wc:
	$(DETEX) $(SOURCES) | wc

.PHONY: clean
clean:
	$(RM) *.dvi *.pdf *.aux *.log

report3.tex

\documentclass[a4paper]{article}
\usepackage{graphicx}
\usepackage{url}
\usepackage{amsmath, amssymb}

\title{Formal Method Report III: Formal Verification and Common Criteria}
\author{Kamiya Shouichi}
\date{February 10, 2012}

\begin{document}
\maketitle
\section*{Introduction}
Nowadays, more and more things were digitized. For example, eBook becomes
popular recentyl due to the release of iBook from Apple Inc. Space development
is one of the most seriouse area and they also rely on computers. Moreover,
even bank accounts are digitized and managed by computers. So it is obviously
important to ensure the quality of softwares somehow, especially in those
serious areas (e.g. space development, banking).

Common Criteria is an international standard for computer security certification
and it can guarantee the certain quality of softwares.\cite{wikipedia:cc} In
Common Criteria Evaluation Assurance Level 7 which is most restrict level
requires formal verification and we can see the importance of formal
verification.

By using formal verification, we can ensure the quality of softwares by proving
or disproving the correctness of the intended algorithms. It is expected that
formal verification can be applied to serious areas such as space develpment.
In fact NASA is using formal verification.\cite{nasa}

\section*{Pros and Cons of Formal Verification}
Following things are thought to be pros of formal verification.\cite{portal}
\begin{list}{}{}
\item We can remove ambiguity from early development phase and understand
  software more. That is much cost in early phase of development and try to
  reduce the cost of fixing bugs in latter development phase.
\item We can prove or disprove the certain property of the system based on
  mathematical theory when the system is very complex or high reliability is
  required.
\end{list}
Following things are thought to be cons of formal verification.\cite{portal}
\begin{list}{}{}
\item Proving or disproving requires requires high cost and consumes much time.
\item It is not still widely adopted in industry and not so many documents are
  available.
\item Not so many people are familiar with formal verification method.
\end{list}

\section*{Discussion}
As we saw in above, formal verification costs a lot of money and time. So it is
not a good idea to use it for products which life cycle is relatively short such
as web development. In web development, requirements are often changes and it is
important to develop and release products.

On the other hand, it is very helpful to use formal verification for systems
where very high reliability is required such as space development. It is hard
and cost a lot of money and time to fix bugs after launching artificial
satelites.

By the way, Common Criteria seems to be losing its popularity unfortunately,
because its sponsors are decreasing year by year.\cite{iccc:2005,iccc:2010,
iccc:2011} In reality, it might cost too much money and time to satisfy Common
Criteria for most of the companies. So more practical version of standard or
formal verification tool might be needed.

\section*{Conclusion}
Formal verification method can be applied to certain field but not every. To
extend applicable field, formal verification need to be more practical.

\begin{thebibliography}{0}
\bibitem{wikipedia:cc}
  \emph{Common Criteria}
  \url{http://en.wikipedia.org/wiki/Common_Criteria}

\bibitem{wikipedia:eal}
  \emph{Evaluation Assurance Level}
  \url{http://en.wikipedia.org/wiki/Evaluation_Assurance_Level}

\bibitem{iccc:2005}
  \emph{ICCC 2005}
  \url{http://www.ipa.go.jp/event/iccc2005/english/index.html}

\bibitem{iccc:2010}
  \emph{ICCC 2010}
  \url{http://www.11iccc.org.tr/}

\bibitem{iccc:2011}
  \emph{ICCC 2011}
  \url{http://12iccc.cybersecurity.my/sponsor.html}

\bibitem{portal}
  \emph{Formal Methods User Group}
  \url{http://fmug.grace-center.jp/taxonomy/term/30}

\bibitem{nasa}
  \emph{NFM 2012 • 4th NASA FORMAL METHODS SYMPOSIUM}
  \url{http://shemesh.larc.nasa.gov/nfm2012/}

\bibitem{gemalto}
  \emph{About the world-first smart card certificate with EAL7 formal assurances}
  \url{http://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf}
\end{thebibliography}
\end{document}