Master in Security of Integrated Systems and Application : Secure your future

Program

Formal Verification (17.5h)

Dominique BORRIONE and Katell MORIN-ALLORY

Design of secure devices

  1. Introduction to integrated systems (7h)
  2. VHDL design (28h)
  3. VHDL synthesis (14h)
  4. Smart cards and silicon technologies (7h)
  5. Design of a cryptographic module (42h)
  6. Integrated circuits test (17.5h)
  7. Formal verification (17.5h)
  8. Embedded systems development (21h)
  9. Hardware security (7h)
  10. Side-channel analysis and counter-measures (28h)
  11. Fault analysis and counter-measures (17.5h)
  12. Bus security and integrated networks (3.5h)

Synopsis

Ensuring the correctness of circuits requires a rigorous design flow. Further to the numeric simulation of test cases, that provides initial confidence in the design, formal methods are subsequently invoked, to validate initial specifications, or prove the correctness of a design step. The Boolean level techniques (BDDs, SAT solving) are now supported by efficient commercial tools, taking as input a "register transfer level" design description in a standard language (Verilog or VHDL), which is automatically transformed into a logic model, allowing the verification, for all possible inputs, that the design performs as expected.
The course is divided in 4 lessons: each lesson comprises a lecture, exercices, and the practical use of specialized software.

Timetable

(A session amounts to 13/4 hours.)
 

Lesson 1-2
General introduction to the formal verification of circuits: why, when, how.
Combinational circuits equivalence
Binary Decision Diagrams, principles, use, examples.

Lesson 3-4
Synchronous sequential circuits: characterization on the VHDL synthezizable subset
The Finite State Machine (FSM) model of a sequential circuit: state space traversal
Sequential circuit equivalence

Lesson 5-6
Expressing properties about circuits (Temporal Logics, CTL)
The verification of temporal properties: model checking, bounded model checking
The SAT (satisfiability) problem (and its solutions)
Application to the verification of properties over the FSM of a circuit

Lesson 7-8
A standard language for property specification: PSL
Assertion-based verification: writing and verifying properties along the design flow, formal and semi-formal property verification.


Back to Program Detail How to apply Contact us
counter-measures   design of secure devices   ecole des mines de saint etienne   embedded security   engineering and security standards   leti   master in security of integrated systems & applications   microelectronics design   nxp   postgraduate certificate   postgraduate courses   postgraduate diploma   postgraduate program   secured design   security engineering   security methodology   security methods   security technology   stmicroelectronics   texas instruments   cryptographics tools   cryptography algorithm   cryptography and applications   cryptography and network security   cryptography and security   cryptography engineering   cryptography network security   cryptography security   cryptography software   cryptography techniques   cryptography theory and practice   cryptography theory   encryption methods   encryption techniques   encryption technology   master in cryptography   postgraduate studies   postgraduate study   system security cryptography   techniques in cryptography   computer security technology   cryptographic module   design of a cryptographic module   gemalto   hardware protection   hardware security   integrated systems   management of hardware security   master in design of hardware security   master in hardware security   network security hardware   security hardware   security of information systems   security techniques   smart card   systems security   vhdl design   vhdl