Ta Vinh Thong

Ta Vinh Thong, PhD. Candidate

Advisor:
Levente, BUTTYÁN, PhD. associate professor

Address: H-1521 Budapest Pf. 91., Hungary
Office: Budapest, XI. Magyar tudósok körútja 2.
Room: I.E.429
Phone: + 36 1 463-2063, Fax: +36 1 463 3266
E-mail: vinhthong.ta (*) crysys.hit.bme.hu, tavinh (*) hit.bme.hu

Short biography:

Ta Vinh Thong was born in 1983 in Hanoi, the capital city of Vietnam. Thong came to Hungary when he was 9 ages old in 1992. He received the MSc degree in computer science from the Budapest University of Technology and Economics (BUTE). Since 2007 he has been working at the Laboratory of Cryptography and System Security (CrySyS) as a research assistant and PhD student.

Schools:

2002: Fazekas Mihály Fõvárosi Gyakorló Gimnázium, Budapest, Hungary.

Special Mathematics class.

2008: MSc Degree at Budapest University of Technology and Economics (BUTE), Budapest, Hungary.

In computer science and IT security.

2008- : PhD student at Laboratory of Cryptography and System Security (CrySyS), BUTE.

My research area: Formal analysis of security protocols and APIs.

International courses I have taken part in :

2008: SWING, PhD School on Security of Wireless Networking. Bertinoro, Italy. Lecturers :

Prof. Srdjan Capkun (ETH Zurich, Switzerland), and
Prof. Michael Reiter (University of North Carolina, USA).

Research activities

Security API analysis.
Hardware Security Modules (HSM) are indispensable in many applications, such as ATM networks, public key infrastructures, electronic ticketing in public transportation, electronic payment systems, and electronic commerce, in general. A HSM is a hardware device (including the firmware and software components) which has some tamper resistance properties, and it is used to store cryptographic keys and to perform various security-critical cryptographic operations. Besides physical tampering and side channel attacks, HSMs can also be attacked through their APIs by exploiting some design weaknesses in the API's logic. Being fully software based, this kind of attacks is much less expensive than physical and side-channel attacks, and depending on the weaknesses that are exploited, it may have devastating effects. One promising approach of API analysis is to apply some formal verification method such as those used in software engineering. We follow this approach, and propose an API verification method based on the applied pi-calculus that seems to be extremely well-suited for the formal modeling of security APIs, the precise definition of the security requirements, and the rigorous analysis of the provided security properties. We demonstrate our approach through the analysis of the SeVeCom HSM API. (See the poster of this topic.)
Security verification of firewalls.
Firewalls are routinely used today to protect internal networks from attacks originating from the Internet. However, firewalls are often misconfigured leaving security holes in the defense system. As firewalls can be stateful and firewall rule sets may contain a very large number of rules, such misconfigurations are hard to discover by informal analysis. We are investigating how formal verification techniques can be used to alleviate this problem.(See the poster of this topic.)
Formal and Automatic security verification of secure routing protocols.
Ad-hoc networks are not based on pre-defined topology, thus, before each data exchange a route discovery is accomplished. The route discovery procedures are defined by routing protocols. Numerous attacks against routing protocols have been published, in which the attacker can achieve that the honest nodes attempt to exchange data through the route that does not exist. This type of attacks is critical because they can lead to futile energy consumption and degrade the efficiency of the network.(See the poster of this topic.)

Publications
Conferences and Journals

[1] L. Buttyán, Ta Vinh Thong, Biztonsági API analízis a spi-kalkulussal, Hiradástechnika, Volume LXIII. , number 8, 2007, 16–21. (PDF)

[2] L. Buttyán, Ta Vinh Thong, Security API analysis with the spi-calculus, Hiradástechnika, Volume LXII. , number 1, 2008, 43–49. (PDF)

[3] L. Buttyán, G. Pék, Ta Vinh Thong, Consistency verification of stateful firewalls is not harder than the stateless case, Infocommunications Journal, Volume LXIV., number 2009/2-3., 2–3, 2009 (PDF)

[4] L. Buttyán, Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking, IFIP Wireless and Mobile Networking Conference (WMNC’2010). (PDF)

[5] F. Kargl, P. Papadimitratos, L. Buttyan, M. Mueter, E. Schoch, B. Wiedersheim, Ta Vinh Thong, G. Calandriello, A. Held, A. Kung, J.-P. Hubaux, Secure Vehicular Communication Systems: Implementation, Performance, and Research Challenges, IEEE Communications Magazine, Volume 46, number 11, 2008 november (PDF)
[6] L. Buttyán, Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols., Periodica Polytechnica Electrical Engineering Journal, 2011 (To appear)

[7] Ta Vinh Thong, L. Buttyán, On automating the verification of secure ad-hoc network routing protocols, Telecommunication Systems Journal, 2011 (LINK)

Technical Reports

[8] Ta Vinh Thong, Security API analysis with the spi-calculus and the ProVerif tool. 2008, CrySyS Lab., BME. (PDF)

[9] Ta Vinh Thong, Levente Buttyán, Formal Verification of the SeVeCom HSM API with the applied pi-calculus and the ProVerif tool. 2009, CrySyS Lab., BME. (PDF)

[10] Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking. 2012, CrySyS Lab., BME. (PDF)

[11] Ta Vinh Thong, Levente Buttyán, Query Auditing for Protecting Max/Min Values of Sensitive Attributes in Statistical Databases. 2012, CrySyS Lab., BME.

[12] Amit Dvir, Levente Buttyán, Ta Vinh Thong, A Secure Distributed Transport Protocol for Wireless Sensor Networks. 2012, CrySyS Lab., BME.

Prizes/Scholarship

Student scientific conference (TDK) 2007, won 1st prize.
Pollák-Virág prize, 2010.
BME kutatói pályázat award, 2011.
HSN Lab-Ericsson scholarship, 2008-2011.
BME TÁMOP scholarship, 2012-2013.

Projects

SeVeCom: Secure Vehicular Communications EU(027795).
Vehicular communications (VC) and inter-vehicular communications (IVC) bring the promise of improved road safety and optimized road traffic through co-operative systems applications. To this end, a number of initiatives have been launched, such as the Car-2-Car Communication Consortium (C2C-CC) in Europe, or DSRC in North America. A prerequisite for the successful deployment of vehicular communications is to make them secure. For example, it is essential to make sure that life-critical information cannot be modified by an attacker; it should also protect as far as possible the privacy of the drivers and passengers. The specific operational environment (moving vehicles, sporadic connectivity, ...) makes the problem very novel and challenging. SeVeCom addresses security of future vehicle communication networks, including both the security and privacy of inter-vehicular and vehicle-infrastructure communication. Its objective is to define the security architecture of such networks, as well as to propose a roadmap for progressive deployment of security functions in these networks. (Website.)
WSAN4CIP: Wireless Sensor and Actuator Networks for Critical Infrastructure Protection (EU FP7 STREP).
The goal of WSAN4CIP is to advance the technology of Wireless Sensor and Actuator Networks (WSANs) beyond the current state of the art, in order to improve the protection of Critical Infrastructures (CIs). By advancing WSAN technology, the project will contribute to networked information and process control systems which are more secure and resilient. The distributed nature of WSANs enables them to survive malicious attacks as well as accidents and operational failures. It makes them dependable in critical situations, when information is needed to prevent further damage to CIs. (Website.)
CHIRON: CYCLIC AND PERSON-CENTRIC HEALTH MANAGEMENT (EU ARTEMIS IP).
The CHIRON Project intends to combine state-of-the art technologies and innovative solutions into an integrated framework designed for an effective and person-centric health management along the complete care cycle. In this vision, CHIRON will address and harmonize the needs and interests of all the three main beneficiaries of the healthcare process, i.e. the citizens using the services, the medical professionals and the whole community. CHIRON will also position the citizens at the core of the whole healthcare cycle by considering them as “persons” with specificities and identities and will empower them to manage their own health. Then, CHIRON will enlarge the boundaries of healthcare by fostering a seamless integration of clinical setting, at home setting and mobile setting in a concept of a continuum of care. this will speed up the move from treatment of acute episodes to prevention. The project will provide the physicians with extensive support for treatment monitoring and management, timely decisions and appropriate actions in both the clinical and home environments.(Website.)

Talks :

Student scientific conference (TDK), 2007.
Departmental PhD students workshop, 2009.
Departmental PhD students workshop, 2010.
WMNC 2010, Budapest.
Thesis discussion, HSN Lab, 2011.
Lecture about the ProVerif tool, 2011.

Teaching activities:

Security of Telecommunication Systems I. (BMEVIHIM220)
Security of Telecommunication Systems II. (BMEVIHIM305)
Laboraroty Exercises I (Faculty of Computer Science).
Laboraroty Exercises II (Faculty of Computer Science).

Talented students I have worked with as their advisor :

Pék Gábor, BSc.

The title of his BSc. thesis: "Security verification of stateful firewalls".

Nguyen Thi Hoang Phuong (Fanni), MSc.

The title of her MSc. thesis: "Formal verification of firewalls".

Zsurkó Mátyás Lehel, MSc.

The title of his MSc. thesis: "Automated security verification of routing protocols".

Languages :

Vietnamese: native.
Hungarian: fluently.
English: read, written and spoken well.

Hobbys:

Playing and watching football.
Spending time with friends and family.
Go to cinema, theatre.

Back