Page 154 - My FlipBook
P. 154
研
人 Research Fellow
員 王柏堯 Bow-Yaw Wang
Faculty Ph.D., Computer Science, University of Pennsylvania, United States
T +886-2-2788-3799 ext. 1717 E bywang@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/~bywang
・ Research Fellow, Institute of Information Science, Academia Sinica (2012-present)
・ Professor (Adjunct), National Taiwan University (2013-present)
・ Associate Research Fellow, Institute of Information Science, Academia Sinica (2008-
2012)
・ Associate Professor (Adjoint), National Taiwan University (2009-2012)
・ Invited Professor, INRIA, France (2009-2011)
・ Assistant Research Fellow, Institute of Information Science, Academia Sinica (2003-2008)
・ Invited Associate Professor, Tsinghua University, China (2009-2010)
・ Assistant Professor (Adjoint), National Taiwan University (2004-2009)
Research Description
My research interests include computational logic, automata theory and formal veri cation, especially including model checking. Formal
verification is a mathematical and logic method that checks properties about computer systems. Among several techniques in formal
veri cation, I am most interested in model checking. Given a formal property and a system description, a model checker veri es whether the
system description conforms to the property. The model checking problem, in general, is computationally di cult, and therefore I have been
developing algorithms and heuristics to improve e ciency.
In recent years, my research interests have focused an applying formal veri cation to practical cryptography. Modern cryptography such as
Elliptic Curve Cryptography requires computation over large nite elds. Commodity computing devise, however, do not support arithmetic
computation on 255-bit integers, for example. Hence, arithmetic over large nite eld needs to be implemented with 64- or 32-bit machine
instructions. If such implementations are incorrect, any security guarantees of cryptosystems would be lost. It is therefore of utmost
importance to formally verify cryptographic programs deployed in computing devices. Along with my colleagues, we have successfully
veri ed several group and eld operations implemented in several security libraries.
I have also worked in formal privacy analysis. Privacy has been one of the most concerned issues in data analyses. Using advanced computing
devices and machine learning techniques, digital personal information is collected and analyzed constantly. The scandal of Facebook and
Cambridge Analytica is perhaps one of the most vivid massive privacy intrusion known to us. Since all data analyses are performed by
programs, I have been applying formal techniques to verifying privacy properties on models of data analysis programs. Speci cally, data
analysis programs are formalized as randomized algorithms in the di erential privacy framework. I have developed veri cation theories for
di erential privacy on probabilistic models.
Publications grained Control on Distributed Data Analytic (poster). 39th
International Conference on Software Engineering (ICSE 2017),
1. Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow- Buenos Aires, Argentina. May 2017.
Yaw Wang, and Bo-Yin Yang. Signed Cryptographic Program
Verification with Typed Cryptoline. 26 th ACM SIGSAC 7. Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengal, Shin-Cheng Mu,
Conference on Computer and Communications Security (CCS Nishant Sinha,and Bow-Yaw Wang. An Executable Sequential
2019), London, UK. November 2019. Specification for Spark Aggregation. 5th International Conference
on Networked Systems (NETYS 2017), Marrakech, Morocco.
2. Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and May 2017.
Bo-Yin Yang. Verifying Arithmetic in Cryptographic C Programs.
34th IEEE/ACM International Conference on Automated Software 8. Fei He, Shu Mao, and Bow-Yaw Wang. Learning-based Assume-
Engineering (ASE 2019), San Diego, USA. November 2019. Guarantee Regression Verification. 28th International Conference
on Computer Aided Verification (CAV 2016), Toronto, Ontario,
3. Depeng Liu, Bow-Yaw Wang, and Lijun Zhang. Model Checking Canada. July 2016.
Differentially Private Properties. 16th Asian Symposium
on Programming Languages and Systems (APLAS 2018), 9. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengal, Tsung-Ju Lii, Ming-
Wellington, New Zealand. December 2018. Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC Learning-
Based Verification and Model Synthesis. 38th International
4. Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Conference on Software Engineering (ICSE 2016), Austin, USA.
Yang. Verifying Arithmetic Assembly Programs in Cryptographic May 2016.
Primitives (invited). 29th International Conference on Concurrency
Theory (CONCUR 2018), Beijing, China. September 2018. 10. Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and
Lijun Zhang. Learning Weighted Assumptions for Compositional
5. Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified Verification of Markov Decision Processes. ACM Transactions
Verification of Algebraic Properties on Low-Level Mathematical Software Engineering and Methodology (TOSEM). 25(3): 21:1-
Constructs in Cryptographic Programs. ACM Conference on 21:39 (2016).
Computer and Communications Security (CCS 2017), Dallas,
USA. October 2017.
6. Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, and Bow-
Yaw Wang. PSpec: A Formal Specification Language for Fine-
152
人 Research Fellow
員 王柏堯 Bow-Yaw Wang
Faculty Ph.D., Computer Science, University of Pennsylvania, United States
T +886-2-2788-3799 ext. 1717 E bywang@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/~bywang
・ Research Fellow, Institute of Information Science, Academia Sinica (2012-present)
・ Professor (Adjunct), National Taiwan University (2013-present)
・ Associate Research Fellow, Institute of Information Science, Academia Sinica (2008-
2012)
・ Associate Professor (Adjoint), National Taiwan University (2009-2012)
・ Invited Professor, INRIA, France (2009-2011)
・ Assistant Research Fellow, Institute of Information Science, Academia Sinica (2003-2008)
・ Invited Associate Professor, Tsinghua University, China (2009-2010)
・ Assistant Professor (Adjoint), National Taiwan University (2004-2009)
Research Description
My research interests include computational logic, automata theory and formal veri cation, especially including model checking. Formal
verification is a mathematical and logic method that checks properties about computer systems. Among several techniques in formal
veri cation, I am most interested in model checking. Given a formal property and a system description, a model checker veri es whether the
system description conforms to the property. The model checking problem, in general, is computationally di cult, and therefore I have been
developing algorithms and heuristics to improve e ciency.
In recent years, my research interests have focused an applying formal veri cation to practical cryptography. Modern cryptography such as
Elliptic Curve Cryptography requires computation over large nite elds. Commodity computing devise, however, do not support arithmetic
computation on 255-bit integers, for example. Hence, arithmetic over large nite eld needs to be implemented with 64- or 32-bit machine
instructions. If such implementations are incorrect, any security guarantees of cryptosystems would be lost. It is therefore of utmost
importance to formally verify cryptographic programs deployed in computing devices. Along with my colleagues, we have successfully
veri ed several group and eld operations implemented in several security libraries.
I have also worked in formal privacy analysis. Privacy has been one of the most concerned issues in data analyses. Using advanced computing
devices and machine learning techniques, digital personal information is collected and analyzed constantly. The scandal of Facebook and
Cambridge Analytica is perhaps one of the most vivid massive privacy intrusion known to us. Since all data analyses are performed by
programs, I have been applying formal techniques to verifying privacy properties on models of data analysis programs. Speci cally, data
analysis programs are formalized as randomized algorithms in the di erential privacy framework. I have developed veri cation theories for
di erential privacy on probabilistic models.
Publications grained Control on Distributed Data Analytic (poster). 39th
International Conference on Software Engineering (ICSE 2017),
1. Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow- Buenos Aires, Argentina. May 2017.
Yaw Wang, and Bo-Yin Yang. Signed Cryptographic Program
Verification with Typed Cryptoline. 26 th ACM SIGSAC 7. Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengal, Shin-Cheng Mu,
Conference on Computer and Communications Security (CCS Nishant Sinha,and Bow-Yaw Wang. An Executable Sequential
2019), London, UK. November 2019. Specification for Spark Aggregation. 5th International Conference
on Networked Systems (NETYS 2017), Marrakech, Morocco.
2. Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and May 2017.
Bo-Yin Yang. Verifying Arithmetic in Cryptographic C Programs.
34th IEEE/ACM International Conference on Automated Software 8. Fei He, Shu Mao, and Bow-Yaw Wang. Learning-based Assume-
Engineering (ASE 2019), San Diego, USA. November 2019. Guarantee Regression Verification. 28th International Conference
on Computer Aided Verification (CAV 2016), Toronto, Ontario,
3. Depeng Liu, Bow-Yaw Wang, and Lijun Zhang. Model Checking Canada. July 2016.
Differentially Private Properties. 16th Asian Symposium
on Programming Languages and Systems (APLAS 2018), 9. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengal, Tsung-Ju Lii, Ming-
Wellington, New Zealand. December 2018. Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC Learning-
Based Verification and Model Synthesis. 38th International
4. Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Conference on Software Engineering (ICSE 2016), Austin, USA.
Yang. Verifying Arithmetic Assembly Programs in Cryptographic May 2016.
Primitives (invited). 29th International Conference on Concurrency
Theory (CONCUR 2018), Beijing, China. September 2018. 10. Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and
Lijun Zhang. Learning Weighted Assumptions for Compositional
5. Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified Verification of Markov Decision Processes. ACM Transactions
Verification of Algebraic Properties on Low-Level Mathematical Software Engineering and Methodology (TOSEM). 25(3): 21:1-
Constructs in Cryptographic Programs. ACM Conference on 21:39 (2016).
Computer and Communications Security (CCS 2017), Dallas,
USA. October 2017.
6. Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, and Bow-
Yaw Wang. PSpec: A Formal Specification Language for Fine-
152
