هل تعتقد أن هناك شيئا رائعا لضمان عدم وجود ثغرات في القانون؟ هل تعتقد أن هناك طريقة للتأكد من أن الناس يمكن أن يكتب هذه المدونة خالية من الشوائب؟ هذا يبدو غير واقعي جدا، ولكن CertiK من المنتخب الصيني من جامعة ييل وكولومبيا والخلفيات، وتحاول تقديم مثل هذه الخدمات تحقق الامن للقراصنة للحوادث المتكررة للصناعة سلسلة كتلة، ووضع معايير السلامة.

 CertiK وقد شارك في تأسيسه من قبل قسم علوم الحاسبات في جامعة ييل البروفيسور شاو تشونغ يو Gurong زارة هوى علوم الحاسب في جامعة كولومبيا، وقد تم تأسيسها رسميا في نهاية عام 2017 في نيويورك وادي السليكون، والتكنولوجيا الأساسية لتطبيق التحقق الرسمي (التحقق الرسمي)، ينص على تطبيق العقود ذكية وسلسلة كتلة مصادقة والحلول الأمنية الايكولوجية.

خريطة | CertiK المؤسس المشارك هوى Gurong (مصدر: DeepTech)

قفزت 2018 حوادث الأمن الميداني العالمي سلسلة كتلة 5-8 مرات

في الوقت الحاضر، وسلسلة كتلة تسمى أعلى المخاطر، والأكثر عرضة للهجمات القراصنة، واحدة من أدنى المعدلات في الصناعة ومجال التوعية بالسلامة. ووفقا للإحصاءات مختلفة، في 2018 وقعت سلسلة كتلة العالمية في مجال لا يقل عن مائة الحوادث الأمنية، وفي عام 2017 قفزت 5-8 مرات مقارنة. المبلغ الإجمالي للخسائر بين 20 $ و 3.8 مليار $، مقارنة مع إجمالي القيمة السوقية الحالية للتشفير العملات العالمية، ولكن أيضا عن 170 مليار $، ونسبة الخسارة من هذا الأمن هو في الحقيقة عالية بشكل مخيف.

الهجمات الأمنية في شكل سلسلة لا نهاية لها كتلة، نظرة الطبقات، من طبقة البيانات، طبقة الشبكة، طبقة من الآراء، طبقة الحوافز والعقود طبقة لطبقة التطبيقات، يمكن أن يكون وسيلة لقطع في الهجوم. ومن بين هذه هي معظم الهجمات طبقة التطبيقات، ويعتبر عقد أكثر ذكاء أن الحوادث الأمنية سلسلة كتلة الأكثر تضررا، ومعظم الحالات الكلاسيكية هي 2016 "داو" الحادث، قراصنة استخدامها لمركز صندوق رأس المال الاستثماري "إن DAO" من ذكية عقد ثغرة، إيثرنت وسرقوا 3.6 مليون دولار (50 مليون ثم تصل قيمتها إلى حوالي $)، وأخيرا اضطر ساحة إيثرنت بأكمله اتخاذ تدابير جذرية لإنشاء التشعب دفاعي الشاق من أجل تعويض خسائرهم.

وCertiK حتى الآن التي تراكمت لديها أكثر من 150 عميلا مع خدمات مصادقة آمنة، وكثير منها ترتبط الأصول منصة التشفير تحمي قيمتها ما يقرب من 1.3 مليار $ في الأصول تحرير الرقمي للهجوم من قبل قراصنة الكمبيوتر، وحافظ على "معدل الحوادث الصفر". السجلات.

وتضم قائمة عملاء أمنها عملة، عملة النار، OKEX، القارة قليلا، مؤسسة إيثرنت ساحة، والتشفير الكم وغيرها من سلسلة العملة سلسلة كتلة مع الشركات الرائدة في صناعة. أكتوبر الماضي، CertiK الحصول على النقود ذراع الاستثمار - الملايين من الدولارات من أموال الاستثمار حاضنة الأمن Binance مختبرات. وقالت متحدثة العملة حاضنة الرئيس التنفيذي تشانغ لينغ (ايلا تشانغ)، CertiK "حل سلسلة كتلة بيئة اليوم في نقطة الألم الحرجة، وفي الوقت نفسه حماية المستخدمين تجارتنا، تتحول تدريجيا معيار الصناعة على المعاملات النقدية."

خريطة | تأسست CertiK أكثر من انجاز السنة لا فيجى (المصدر: CertiK)

وCertiK يمكن أن يكون هناك ضمان بأن الضعف رمز الخدمة مصادقة آمنة، والتكنولوجيا الأساسية هو في الواقع إدخال اثنين من المؤسسين وGurong هوى سنوات من البحث في "التحقق الرسمي" (التحقق الرسمي) المجال، ولعب مكافحة CertiKOS كان الهاكرز نظام التشغيل نظام في عام 2016 تقدمت وزارة الدفاع الامريكية وكالة مشاريع البحوث (DARPA) بتمويل "شبكة ضمان عالية من الأنظمة العسكرية (HACMS)" اعتمدت باعتبارها واحدة من المكونات الأساسية للنظام.

تحقق الرسمي، أي شعب للكتابة استغلال كود

ما هي تقنية التحقق الرسمية؟ جعل الناس فعلا كتابة التعليمات البرمجية خالية من الشوائب؟

باختصار، التحقق الرسمي هو حساب التفاضل والتكامل من المنطق بالمنطق الرياضي لإثبات أن البرنامج من جهة نظر رياضية، والبرمجيات، أو عقد الذكية، لا يوجد الثغرات الأمنية. وسيكون لكل إثبات القيام على ثبت منطقيا. قبل التحقق الرسمي، قد يكون مثل هذا البرنامج نفس دليلا على نظرية رياضية، في أي اختبارات الحالة هي التأكد من الحصول على النتيجة الصحيحة.

Gurong هوى تفسير DeepTech، تكنولوجيا السلامة العامة عادة في محاولة للعثور على الثغرات الممكنة، أو لضمان درجة كبيرة على الاحتمال لا يمكن أن تذهب الخطأ، ولكن التحقق الرسمي هو أن تكون قادرة على إثبات مباشرة من البرنامج الصحيح رياضيا، "هو حاليا على أعلى مستوى معروف للأمن تقنية".

وهذا هو، التحقق الرسمي، بطريقة يمكن للناس أن كتابة التعليمات البرمجية التي يمكن أن تضمن أي الضعف.

واضاف "بالطبع، ويستند هذا على نموذج رياضي من صحتها، يجب أن تعتمد على الكثير من المباني والافتراضات"، وأضاف Gurong هوى "، ولكن إذا كان يمكن أن تتحقق شروط مسبقة لها، ثم في نهاية المطاف سوف يجتمع مستوى أمنها أعلى من غيرها من التكنولوجيات ".

التحقق الرسمي هو في الواقع من 1960s و 1970s في الاتجاه الأبحاث بدأ في الارتفاع، ولكن بسبب زيادة الاحتياجات من تطبيق الشروط، لا يمكن التعامل مع البرمجيات ونظم أكثر تعقيدا، في معظم الحالات العملية، والإعمال الكامل الإثبات الرسمي صعبة للغاية. لذلك كان إثبات رسمي في اختراق تقني محدود، والدولة هي أيضا مثالية لتطبيقات ميدانية لا يمكن أن تجد. حتى حوالي عام 2015، وسيتم المتراكمة Gurong هوى شاو التحقق الرسمي على مر السنين في مجال البحوث، بحوث محددة والتطوير في عمق مواصفات، والتسلسل الهرمي وغيرها من التكنولوجيا، فقد اكتسب اختراق أكثر أهمية.

أما وقد قلت ذلك، للتحقق الرسمي للتطبيق السيناريو، لا تزال منحازة لصالح رمز ليست معقدة جدا، والظروف هي بسيطة نسبيا، ولكن البرامج ذات القيمة العالية. سلسلة كتلة يناسب هذه الخصائص، لأن سلاسل كتلة غالبا ما كمية من التعليمات البرمجية محدودة نسبيا لتشفير الأصول عالية القيمة المقابلة، وشروط المتعرجة ويمكن السيطرة عليها نسبيا. الأهم من ذلك، ويرجع ذلك إلى سلسلة كتلة لا يمكن تغييرها، وإصلاحات كود علة صعبة، حتى للتحقق الرسمي من هذه التكنولوجيا.

لهذا السبب، في عام 2017 يتزامن مع سلسلة كتلة بيتكوين ارتفعت مدفوعا التطور التكنولوجي، CertiK العثور بسرعة على وضعهم في هذه الصناعة، وإدخال منصة التحقق الرسمية، وتوفير سلسلة كتلة لتشمل جميع مكونات عقود ذكية النظام الإيكولوجي، DApps الخ خدمة التدقيق الأمني.

بعبارات بسيطة، خدمات CertiK من خلال الهيكل الهرمي للنظام معقد ليتم التحقق من صحة قبل التصفيف، وحدة البرمجيات تقسيم، ومن ثم استخدام المواصفات عمق أثبتت معقدة للتحقق ما إذا كان كل الطبقات ضمن مواصفات . بهذه الطريقة، يمكنك في الوقت نفسه تعزيز المرونة والكفاءة للتحقق الأمن، وسيتم تطبيق التحقق الرسمي في سيناريوهات الأعمال محددة.

عملة مستقرة للعملاء، على سبيل المثال، CertiK عقودها الذكية القيام به هو كتابة أول ما نزل مواصفات العقد في شكل ملصقات، وأدى ذلك إلى انقسام المجمع في عقود أصغر وحدة الاستخبارات يمكن التحقق منها، على مستويات مختلفة من التجريد طبقة واقية. ثم ثبت أخيرا وحدة مجتمعة، تولد صلاحية شهادة العقد بأكمله.

خريطة | استخدام "المعايير عميقة" عقود حماية ذكية (المصدر: CertiK)

عقود للغة البرمجة الذكية أعماق البحار

تحليل Gurong هوى، وقد تم صناعة سلسلة كتلة الحوادث الأمنية المتكررة للغاية، ويرجع ذلك جزئيا صناعة الوعي بالسلامة منخفضة عموما، ونقص الوعي التكنولوجيا الأمنية، فإن عددا من المشاريع كتل سلسلة أو منصة لا يعطي الأولوية لاعتبارات أمنية، لا أريد أن بناء الأمن الاستثمار. وحتى أولئك الذين الانتباه إلى بر الأمان، وأنا لا أعرف كيف لاختيار، قد دفع التكلفة العالية، ولكن للحصول على نعمة الأمن محدودة جدا.

من ناحية أخرى، تكمن المشكلة في أدوات التطوير المعتادة كتلة سلسلة صناعة. وأشار Gurong هوى إلى أن منع الآن المبرمجين سلسلة صناعة عموما مثل استخدام C ++ أو بيثون لكتابة العقود ذكية، ولكن هذه الأدوات من وجهة نظر مهنية أمن نظر، هي لغة غير آمنة جدا. ولا سيما بيثون، ولدت ليست مناسبة لتطوير ارتفاع الطلب على أنظمة الأمن.

"لغات مختلفة مثل الأدوات، وهناك الطرق المختلفة المستخدمة، انها مثل عند استخدام كماشة مفك البراغي لجعل". ويعتقد Gurong هوى انه اذا تعتمد هذه الشركات بشكل كبير في اللغات التالية تعمل في مجال تطوير واختبار والتحقق من صحة ما يعادل أقل أمنا فقط بعد فوات الأوان.

ولذلك، CertiK أدخلت مؤخرا لغة برمجة جديدة أعماق البحار، التي هي لغة البرمجة الوظيفية لعقود عقود الذكية الذكية، من خلال إدخال التكنولوجيا التحقق رسمية لضمان عقود الاستخبارات الأمنية.

ووفقا Gurong هوى أوضح، يمكن القول أعماق البحار أن تكون "مترجم خالية من الشوائب" التي يمكن أن تثبت شفرة المصدر من دون ثغرات، يمكنك بناء إطار عبر منصة التي كتبها أعماق البحار-Blockchain، عقد المخابرات موثوق بها، والهدف من ذلك هو Hyperledger، EVM، الخ المطورين على منصة لتوفير بيئة تطوير موثوق آمنة.

"نقطة الانطلاق لدينا هو الأمل في مستوى الرمز مصدر إدخال مفاهيم تصميم آمنة من لغة مصممة لوضع حد لبعض الأخطاء بسيطة جدا في الخزينة في وقت مبكر نسبيا"، وقال Gurong هوى.

منذ إطلاق أعماق البحار، وبدأت بضعة أشهر للحصول على المال البذور كولومبيا -IBM مركز سلسلة كتلة مؤسسة إيثرنت ساحة (مؤسسة Ethereum) جائزة البحوث الخامسة، فضلا عن سلسلة الكم (Qtum) الأموال المخصصة للبحث.

خريطة | فريق CertiK (المصدر: DeepTech)

وبالإضافة إلى ذلك، قال Gurong هوى DeepTech، وقد تم تأسيسها قبل أكثر من عام قرب CertiK، كما بدأت لجمع نحو 30 مليون $. في إطار الدعم المالي، نمت CertiK حجم الفريق إلى أكثر من 20 شخصا، من بينهم المدير التجاري السابق يان ني تريليون دولار في الأعضاء المؤسسين نائب الرئيس R & D جوجل gVisor ويقدم صندوق النقد الدولي (IMF) الاقتصاديين فتح، وفرق فرقت في نيويورك ، سياتل، وبكين، وسول، وسوف تستمر في أن يستكمل هذا العام، أكثر التوسع على نطاق واسع.

تدفق المنح والاستثمار، وتسليط الضوء على صناعة سلسلة كتلة لموثوق بها، بناء الأمن موحدة هناك حاجة ملحة. في الوقت الحاضر، لا تزال البيئة الأمنية التشفير الأصول الهش، ومقدمي الخدمات الأمنية تمنع سلسلة إذا كان يحتوي على CertiK بما في ذلك، فإن نجاح منتجاتها يمكن أن يكون مقبولا على نطاق واسع من جانب الصناعة، ويتوقع أيضا أن تغيير صناعة سلسلة كتلة بيئة بشكل أساسي.