Page 137 - My FlipBook

Brochure 2020
III. Formal Verification on Group and Field Operations in
Cryptographic Programs
Modern cryptography relies on computation over
large finite fields. However, commodity computing
devices do not natively support long integer (such as
255 bits) computation. Therefore, computation over
large finite fields must be implemented on 32- or 64-
bit architectures. Such implementations necessarily
vary depending on the architecture. In OpenSSL,
multiplication over large finite fields has been
implemented for x86, ARM and SPARC. Whether all
assembly programs implement multiplication correctly
is of utmost importance in applications of cryptography.
We are focusing on developing practical and formal
techniques for verifying algebraic properties on group
and field operations in cryptographic programs.
In collaboration with practical cryptographers, our
technique has been applied to verify group and field
operations in various elliptic curve cryptosystems in
OpenSSL, Bitcoin and wolfSSL.
IV. String Constraint Solving
Web program security is a crucial building block of
our digital infrastructure. Among other means of
ensuring cybersecurity, there is an apparent demand
for automatic web program analysis. String constraint
solvers are the engine of modern web program analysis
techniques. Due to high demand, there has been a
considerable increase in the number of publications on
this subject over the past six years. Together with our
close collaborators in Europe, we have achieved a series
of successes in this research direction. For example, we
proposed the first string constraint solving procedure
that is able to generate Craig interpolant, which is
essential in the invariant generation for software
model checking. Our string constraint solver, named
Trau, is among the most efficient implementations in
the world. Nevertheless, current state-of-the-art for
the development of string constraint solvers lags way
behind the levels required for web program analysis and,
together with our colleagues globally, we are working
toward bridging that gap.
V. Communal Sharing of Sensitive Data
Privacy refers not merely to restrictions on acquiring
personal data, but represents a set of principles and rules
that govern the use of information and its disclosure.
How to appropriately manage information flows and
to encourage data sharing yet keep shared information
private remains a challenge. A typical approach is for
a centralized data controller to de-identify a dataset
collected from individuals before it is released for
reuse. That the interests of the three actors involved,
i.e., individuals, data controllers, and third-party data
users, are not properly aligned is a central dilemma in
sharing and reusing personal data. Together with legal
scholars, we are working toward a communal approach
to personal data management whereby, without an
external authority, members of a community can pool
sensitive information about themselves for mutual
benefits. Principles from programming languages and
formal methods will guide us in the development of
good data-sharing schemes with verifiable properties.
We will develop methods, tools, and systems to facilitate
communal management of sensitive data and put them
into use.
VI. Education
In addition to our research activities, we also dedicate
signi cant resources to education. In order to introduce
our research to students, we have organized the
yearly Formosan Summer School on Logic, Language,
and Computation (FLOLAC), in operation since 2007.
Through FLOLAC, more and more students in Taiwan
have been encouraged to study and conduct research
on programming languages and formal methods.
135