Page 38 - 2017 Brochure
P. 38
earch Laboratories
Programming Languages and Formal Methods Lab
The Programming Languages and Formal Methods implementations necessarily vary depending on the
research group develops techniques for ensuring program architecture. In OpenSSL, multiplication over large finite
correctness. Our research into programming languages fields has been implemented for x86, ARM and SPARC.
focuses on syntactic, semantic, and pragmatic issues in Whether all low-level assembly programs implement
the development of correct programs. Our work on formal multiplication correctly is of utmost importance in
methods emphasizes the algorithmic, computational, and cryptography. We focus on developing practical formal
practical aspects of the analysis of realistic programs. techniques for verifying functional properties on low-level
We apply mathematical and formal techniques to the cryptographic programs. In collaboration with practical
investigation of our research problems. We also aim to cryptoanalysts, our technique has been applied to verify
develop tools and methodologies to help developers in the Montgomery Ladderstep for the group operation on the
writing correct codes. secure elliptic curve Curve25519.
1. Verification and Synthesis of MapReduce 3. Reasoning and Derivation of Functional and
Programs Monadic Programs
MapReduce is a popular programming model for data- Purely functional languages, in which functions are
parallel computation, wherein the reducer produces an true mathematical functions, offer a simple model of
output from a list of inputs. Due to the scheduling policy of computation, where programs can be understood as
the platform, inputs may arrive at the reducers in various mathematical equations whose properties can be proved
orders. The commutativity problem of reducers asks if the using mathematical tools, such as induction. One can
output of a reducer is independent of the input order. We derive, from a program specification, an efficient program
proved that the problem is undecidable if the input is a list by stepwise equational reasoning, in which every step is
of mathematical integers, however, the problem becomes justified by some theorem. This technique, called “program
decidable if the inputs are bounded integers (the integers derivation”, aims to provide formalization and patterns
in computers). We also developed an automaton model
for reducers, named register automata over rationals.
The model has many good mathematical properties. For
example, equivalence and commutativity problems can be
decided in polynomial space. We plan to use the model as a
basis for automatic code generation of reducers.
2. Formal Verification on Low-Level
Cryptographic Programs
Modern cryptography relies on computation over large
finite fields. However, commodity computing devices do
not natively support long (255-bit) integer computation.
Therefore, computation over large finite fields must
be implemented with 32- or 64-bit instructions. These
36 研究群 Research Laboratories
Programming Languages and Formal Methods Lab
The Programming Languages and Formal Methods implementations necessarily vary depending on the
research group develops techniques for ensuring program architecture. In OpenSSL, multiplication over large finite
correctness. Our research into programming languages fields has been implemented for x86, ARM and SPARC.
focuses on syntactic, semantic, and pragmatic issues in Whether all low-level assembly programs implement
the development of correct programs. Our work on formal multiplication correctly is of utmost importance in
methods emphasizes the algorithmic, computational, and cryptography. We focus on developing practical formal
practical aspects of the analysis of realistic programs. techniques for verifying functional properties on low-level
We apply mathematical and formal techniques to the cryptographic programs. In collaboration with practical
investigation of our research problems. We also aim to cryptoanalysts, our technique has been applied to verify
develop tools and methodologies to help developers in the Montgomery Ladderstep for the group operation on the
writing correct codes. secure elliptic curve Curve25519.
1. Verification and Synthesis of MapReduce 3. Reasoning and Derivation of Functional and
Programs Monadic Programs
MapReduce is a popular programming model for data- Purely functional languages, in which functions are
parallel computation, wherein the reducer produces an true mathematical functions, offer a simple model of
output from a list of inputs. Due to the scheduling policy of computation, where programs can be understood as
the platform, inputs may arrive at the reducers in various mathematical equations whose properties can be proved
orders. The commutativity problem of reducers asks if the using mathematical tools, such as induction. One can
output of a reducer is independent of the input order. We derive, from a program specification, an efficient program
proved that the problem is undecidable if the input is a list by stepwise equational reasoning, in which every step is
of mathematical integers, however, the problem becomes justified by some theorem. This technique, called “program
decidable if the inputs are bounded integers (the integers derivation”, aims to provide formalization and patterns
in computers). We also developed an automaton model
for reducers, named register automata over rationals.
The model has many good mathematical properties. For
example, equivalence and commutativity problems can be
decided in polynomial space. We plan to use the model as a
basis for automatic code generation of reducers.
2. Formal Verification on Low-Level
Cryptographic Programs
Modern cryptography relies on computation over large
finite fields. However, commodity computing devices do
not natively support long (255-bit) integer computation.
Therefore, computation over large finite fields must
be implemented with 32- or 64-bit instructions. These
36 研究群 Research Laboratories
