Welcome to My World!

{ } About me

I'm a postdoc fellow at Grinnell College, working with Peter-Michael Osera on program synthesis.

Research Interests
Formal Verification, Program Languages, Software Engineering, Systems and Security, Artificial Intelligence as well as theories and applications in practical problems. CV

Before Grinnell
I completed my PhD from Stevens, advised by Prof. Koskinen. I have a strong affinity for mathematical modeling, which dissects practical problems using precise mathematical logics. The abstracted models can then subsequently be employed to address a wide spectrum of real-world challenges, they are great tools to enchance our ability to comprehend and interpret the reality through the lense of software systems.

On the personal side I enjoy sports (workout, running, hiking, swimming), dancing to the music, reading (my bookshelves), and traveling to interesting cities. Ocassionally, I like writing Blogs.

New If you are Grinnell student and would like to do summer research with me, checkout MAP proposal for details!

/> Projects ==>

Foundations and Applications of Constraint-based Synthesis.
Dynamic Temporal Verification. DrNLA
Automatically Verifying Temporal Properties of Lifted Binaries. DarkSea
Mobile Application Data Analysis. 🤖

/> Teaching

Spring 2024 CSC208 Discrete Structures, Grinnell College.

/> Talks

April 2023 Automatic Verification of Lifted Binaries, Empire Hacking, slides.

Nov. 2022 Seminar talk on DrNLA and cybersecurity, Seton Hall University.

Oct. 2022 Research work on DrNLA, NJPLS, slides.

Dec. 2021 Successfully defend my dissertation proposal, slides.

Oct. 2021 Paper presentation on APLAS 2021 📽;

Oct. 2021 Student forum, poster presentation, FMCAD 2021, 📇, 📃.

July 2018 Participant talk on LTL, OPLSS 2018.

/> Community Service

March 2024 Artifact Evaluation Committee, PLDI 2024.

May 2023 Artifact Evaluation Committee, CAV 2023.

July 2022 Paper Review, APLAS 2022.

May 2022 Artifact Evaluation Committee, CAV 2022.

Oct. 2020 Artifact Evaluation Committee, TAP 2021, CGO 2021.

June 2018 Student Volunteer, PLDI 2018.

/> Publications

Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos, Eric Koskinen, and ThanhVu Nguyen. DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing, arXiv:2306.15584.
Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch, Eric Koskinen, Ton-Chanh Le, Georgios Portokalidis, and Jun Xu. Proving LTL Properties of Bitvector Programs and Decompiled Binaries, APLAS 2021.
Yuandong Liu, Yanwei Li, Yanhui Guo and Miao Zhang. Stratify Mobile App Reviews: E-LDA Model Based on Hot Entity Discovery, SITIS 2016.
Shiting Xu, Yuandong Liu, Xinyu Ma, Qiang Sheng. "Malicious Application Dynamic Detection In Real-Time API Analysis", Smart Data 2016.
Wang Sai, Guo Yanhui, Wu Qiuxin, Liu Yuandong. A detection method of Android application malicious behaviors based on Xposed framework, Sciencepaper Online 12: 1264.

/> Mobile Application Data Analysis

When you click the button on your app, what is it really doing?

The mobile data we are studying here is mainly focused on mobile application online reviews, and mobile App API data. Our laboratory have years of experiences in software security analysis, including malicious software detection, code security audit and security reinforcement in software etc.. We thus have collected huge data about the software stored in our local server, and we find out these data are becoming heavier and noiser, in which itself have a great value in informaiton reuse. In this situation, we start this project to clean and reuse the data we have, to make a deeper analysis on these data in different angles, urshering in a new way to study mobile app security.

Users download apps from app stores, and write reviews to share their experiences about the app performance, these reviews contain valuable information for app developers, also attract to latent users. Our work on reivews analysis include features extraction and text classification, as well as sentiment computation etc. With respect to App API, we parse the log file and record the parameter values of API, feeding them with proper mathematical models, by doing this, we propose a novel approach to detect malicious apps, distinguished from our previous works which focus on code analysis.

Facing the huge data computing that consumes great resources, I am also doing some research on algorithm optimization in machine learning, trying to improve the simultaneous matrix diagonalization in principal component analysis(PCA).

Related Work:

  • Yuandong Liu, Yanwei Li, Yanhui Guo and Miao Zhang, "Stratify Mobile App Reviews: E-LDA Model Based on Hot Entity Discovery", confernce: SITIS 2016
  • Shiting Xu, Yuandong, Liu, Yanhui Guo, Guoai Xu, "Malicious Application Dynamic Detection In Real-Time API Analysis", conference: Smart Data 2016

/> Mobile Network Security Authentication System

Is the app safe before it is uploaded to App stores?

Although there are 460 million Adroid active users in China, making it the world's largest Andriod population, only 30% of them can access to Google Play, therefore 70% of users discover daily Android apps through third-party app stores. Android developers are free to distribute their apps in any intended approaches, including publishing into third-party app stores. There are more than ten third-party app stores in China used by local people every day, as a result, the trustworthiness of app stores in China is an open question. This project detect each APK file and repackage it with an authentic signature before upoading to app stores.

The whole procedure of APK detection includes static analysis and dynamic analysis, as well as malicious app searching engine etc.. I am responsible for Android dynamic analysis, based on an open source project Xposed Framework, I developed an Android system API monitor module . The module can record and modified the parameters of API involked by the running app, it can also notify users the details of app behaviors, e.g., text sending, internet connecting, audio recording, camera involking etc..

More Reading:

  • The source code in my charge can be downloaded here
  • I also co-authored a Chinese paper, "A detection method of Android application malicious behaviors based on Xposed framework", Sciencepaper Online 12: 1264

/> Personal Tour Sites Planning System

When you are going to travel places with which you are unfamiliar, how can you schedule your tour sites using your time and money to the limit? Would you like to share your findings with other tourists who haven't been there during your trip?

This project provide tourists a tool to organize their trips according to their personal prefernce, and a community to communicate with people who are mutually fond of same tour sites. The system is designed in three-layer web structure: Business Logic Layer(BLL), Data Access Layer(DAL), User Interface(UI). We build B/S database application system, implemented the system with ASP.net framwork in Visual Studio. We also developed an algorithem to optimize the route for users, presenting the tour sites dynamically on the map by invoking Baidu map API.

The source code can be found here

/> Mathematical Contest in Modeling 2013

How can we determine an effective, feasible, and cost-efficient water strategy to meet the projected water needs of a country in 2025?

At present, the shortage of fresh water resources has seriously restricted the development of many countries in the world, so it is particularly important to develop rational and effective water resources strategies. In order to meet the water demand by 2025, this paper takes China as the research object, analyzes its water resources data, combines with China's economic, ecological and environmental factors, and finally establishes freshwater resources strategic planning model.

In order to solve the problems in the water storage and transportation, seawater desalinization and water resources protection, we made maximization of social benefits S(X) and economic benefits J(X) as the goal, the water storage, transportation, desalinization and water resources protection as the constraint conditions, and set up a multiple objectives programming model. In solving the model, we made the social benefit as the constraint conditions, and then transformed it into a single objective programming model. After the model was solved, the optimal allocation of water resources was achieved. In particular, the application field of the water resources optimal allocation model can be cities, countries and even the whole planet. The model has general applicability. Meanwhile, the model is also applicable to allocation of other resources, such as oil, natural gas, minerals etc..

Full Paper